H-Termination proof of /home/matraf/haskell/eval_FullyBlown

MAYBE 5.066 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could not be shown:

↳ HASKELL

  ↳ IFR

mainModule Main

(((^) :: Float -> Int -> Float) :: Float -> Int -> Float)

module Main where

import qualified Prelude

If Reductions:
The following If expression

if primGEqNatS x y then Succ (primDivNatS (primMinusNatS x y) (Succ y)) else Zero

is transformed to

primDivNatS0 x y True = Succ (primDivNatS (primMinusNatS x y) (Succ y))

primDivNatS0 x y False = Zero

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

mainModule Main

(((^) :: Float -> Int -> Float) :: Float -> Int -> Float)

module Main where

import qualified Prelude

Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

mainModule Main

(((^) :: Float -> Int -> Float) :: Float -> Int -> Float)

module Main where

import qualified Prelude

Cond Reductions:
The following Function with conditions

g x n

| even n

= g (x * x) (n `quot` 2)

| otherwise

= f x (n - 1) (x * y)

is transformed to

g x n = g2 x n

g1 x n True = g (x * x) (n `quot` 2)

g1 x n False = g0 x n otherwise

g0 x n True = f x (n - 1) (x * y)

g2 x n = g1 x n (even n)

The following Function with conditions

f vv 0 y = y

f x n y =

g x n

where

g x n

| even n

= g (x * x) (n `quot` 2)

| otherwise

= f x (n - 1) (x * y)

is transformed to

f vv yu y = f4 vv yu y

f x n y = f0 x n y

f0 x n y =

g x n

where

g x n = g2 x n

g0 x n True = f x (n - 1) (x * y)

g1 x n True = g (x * x) (n `quot` 2)

g1 x n False = g0 x n otherwise

g2 x n = g1 x n (even n)

f3 True vv yu y = y

f3 yv yw yx yy = f0 yw yx yy

f4 vv yu y = f3 (yu == 0) vv yu y

f4 yz zu zv = f0 yz zu zv

The following Function with conditions

^ x 0 = 1

^ x n

| n > 0

= f x (n - 1) x

where

f vv 0 y = y

f x n y =

g x n

where

g x n

| even n

= g (x * x) (n `quot` 2)

| otherwise

= f x (n - 1) (x * y)

^ vw vx = error []

is transformed to

^ x zy = pr4 x zy

^ x n = pr2 x n

^ vw vx = pr0 vw vx

pr0 vw vx = error []

pr2 x n =

pr1 x n (n > 0)

where

f vv yu y = f4 vv yu y

f x n y = f0 x n y

f0 x n y =

g x n

where

g x n = g2 x n

g0 x n True = f x (n - 1) (x * y)

g1 x n True = g (x * x) (n `quot` 2)

g1 x n False = g0 x n otherwise

g2 x n = g1 x n (even n)

f3 True vv yu y = y

f3 yv yw yx yy = f0 yw yx yy

f4 vv yu y = f3 (yu == 0) vv yu y

f4 yz zu zv = f0 yz zu zv

pr1 x n True = f x (n - 1) x

pr1 x n False = pr0 x n

pr2 zw zx = pr0 zw zx

pr3 True x zy = 1

pr3 zz vuu vuv = pr2 vuu vuv

pr4 x zy = pr3 (zy == 0) x zy

pr4 vuw vux = pr2 vuw vux

The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

mainModule Main

(((^) :: Float -> Int -> Float) :: Float -> Int -> Float)

module Main where

import qualified Prelude

Let/Where Reductions:
The bindings of the following Let/Where expression

pr1 x n (n > 0)

where

f vv yu y = f4 vv yu y

f x n y = f0 x n y

f0 x n y =

g x n

where

g x n = g2 x n

g0 x n True = f x (n - 1) (x * y)

g1 x n True = g (x * x) (n `quot` 2)

g1 x n False = g0 x n otherwise

g2 x n = g1 x n (even n)

f3 True vv yu y = y

f3 yv yw yx yy = f0 yw yx yy

f4 vv yu y = f3 (yu == 0) vv yu y

f4 yz zu zv = f0 yz zu zv

pr1 x n True = f x (n - 1) x

pr1 x n False = pr0 x n

are unpacked to the following functions on top level

pr2F3 True vv yu y = y

pr2F3 yv yw yx yy = pr2F0 yw yx yy

pr2Pr1 x n True = pr2F x (n - 1) x

pr2Pr1 x n False = pr0 x n

pr2F0 x n y = pr2F0G y x n

pr2F vv yu y = pr2F4 vv yu y

pr2F x n y = pr2F0 x n y

pr2F4 vv yu y = pr2F3 (yu == 0) vv yu y

pr2F4 yz zu zv = pr2F0 yz zu zv

The bindings of the following Let/Where expression

g x n

where

g x n = g2 x n

g0 x n True = f x (n - 1) (x * y)

g1 x n True = g (x * x) (n `quot` 2)

g1 x n False = g0 x n otherwise

g2 x n = g1 x n (even n)

are unpacked to the following functions on top level

pr2F0G0 vuy x n True = pr2F x (n - 1) (x * vuy)

pr2F0G vuy x n = pr2F0G2 vuy x n

pr2F0G1 vuy x n True = pr2F0G vuy (x * x) (n `quot` 2)

pr2F0G1 vuy x n False = pr2F0G0 vuy x n otherwise

pr2F0G2 vuy x n = pr2F0G1 vuy x n (even n)

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

mainModule Main

(((^) :: Float -> Int -> Float) :: Float -> Int -> Float)

module Main where

import qualified Prelude

Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                      ↳ Narrow

mainModule Main

((^) :: Float -> Int -> Float)

module Main where

import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="(^)",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="(^) vuz3",fontsize=16,color="grey",shape="box"];3 -> 4[label="",style="dashed", color="grey", weight=3];
4[label="(^) vuz3 vuz4",fontsize=16,color="black",shape="triangle"];4 -> 5[label="",style="solid", color="black", weight=3];
5[label="pr4 vuz3 vuz4",fontsize=16,color="black",shape="box"];5 -> 6[label="",style="solid", color="black", weight=3];
6[label="pr3 (vuz4 == fromInt (Pos Zero)) vuz3 vuz4",fontsize=16,color="black",shape="box"];6 -> 7[label="",style="solid", color="black", weight=3];
7[label="pr3 (primEqInt vuz4 (fromInt (Pos Zero))) vuz3 vuz4",fontsize=16,color="burlywood",shape="box"];1961[label="vuz4/Pos vuz40",fontsize=10,color="white",style="solid",shape="box"];7 -> 1961[label="",style="solid", color="burlywood", weight=9];
1961 -> 8[label="",style="solid", color="burlywood", weight=3];
1962[label="vuz4/Neg vuz40",fontsize=10,color="white",style="solid",shape="box"];7 -> 1962[label="",style="solid", color="burlywood", weight=9];
1962 -> 9[label="",style="solid", color="burlywood", weight=3];
8[label="pr3 (primEqInt (Pos vuz40) (fromInt (Pos Zero))) vuz3 (Pos vuz40)",fontsize=16,color="burlywood",shape="box"];1963[label="vuz40/Succ vuz400",fontsize=10,color="white",style="solid",shape="box"];8 -> 1963[label="",style="solid", color="burlywood", weight=9];
1963 -> 10[label="",style="solid", color="burlywood", weight=3];
1964[label="vuz40/Zero",fontsize=10,color="white",style="solid",shape="box"];8 -> 1964[label="",style="solid", color="burlywood", weight=9];
1964 -> 11[label="",style="solid", color="burlywood", weight=3];
9[label="pr3 (primEqInt (Neg vuz40) (fromInt (Pos Zero))) vuz3 (Neg vuz40)",fontsize=16,color="burlywood",shape="box"];1965[label="vuz40/Succ vuz400",fontsize=10,color="white",style="solid",shape="box"];9 -> 1965[label="",style="solid", color="burlywood", weight=9];
1965 -> 12[label="",style="solid", color="burlywood", weight=3];
1966[label="vuz40/Zero",fontsize=10,color="white",style="solid",shape="box"];9 -> 1966[label="",style="solid", color="burlywood", weight=9];
1966 -> 13[label="",style="solid", color="burlywood", weight=3];
10[label="pr3 (primEqInt (Pos (Succ vuz400)) (fromInt (Pos Zero))) vuz3 (Pos (Succ vuz400))",fontsize=16,color="black",shape="box"];10 -> 14[label="",style="solid", color="black", weight=3];
11[label="pr3 (primEqInt (Pos Zero) (fromInt (Pos Zero))) vuz3 (Pos Zero)",fontsize=16,color="black",shape="box"];11 -> 15[label="",style="solid", color="black", weight=3];
12[label="pr3 (primEqInt (Neg (Succ vuz400)) (fromInt (Pos Zero))) vuz3 (Neg (Succ vuz400))",fontsize=16,color="black",shape="box"];12 -> 16[label="",style="solid", color="black", weight=3];
13[label="pr3 (primEqInt (Neg Zero) (fromInt (Pos Zero))) vuz3 (Neg Zero)",fontsize=16,color="black",shape="box"];13 -> 17[label="",style="solid", color="black", weight=3];
14[label="pr3 (primEqInt (Pos (Succ vuz400)) (Pos Zero)) vuz3 (Pos (Succ vuz400))",fontsize=16,color="black",shape="box"];14 -> 18[label="",style="solid", color="black", weight=3];
15[label="pr3 (primEqInt (Pos Zero) (Pos Zero)) vuz3 (Pos Zero)",fontsize=16,color="black",shape="box"];15 -> 19[label="",style="solid", color="black", weight=3];
16[label="pr3 (primEqInt (Neg (Succ vuz400)) (Pos Zero)) vuz3 (Neg (Succ vuz400))",fontsize=16,color="black",shape="box"];16 -> 20[label="",style="solid", color="black", weight=3];
17[label="pr3 (primEqInt (Neg Zero) (Pos Zero)) vuz3 (Neg Zero)",fontsize=16,color="black",shape="box"];17 -> 21[label="",style="solid", color="black", weight=3];
18[label="pr3 False vuz3 (Pos (Succ vuz400))",fontsize=16,color="black",shape="box"];18 -> 22[label="",style="solid", color="black", weight=3];
19[label="pr3 True vuz3 (Pos Zero)",fontsize=16,color="black",shape="box"];19 -> 23[label="",style="solid", color="black", weight=3];
20[label="pr3 False vuz3 (Neg (Succ vuz400))",fontsize=16,color="black",shape="box"];20 -> 24[label="",style="solid", color="black", weight=3];
21[label="pr3 True vuz3 (Neg Zero)",fontsize=16,color="black",shape="box"];21 -> 25[label="",style="solid", color="black", weight=3];
22[label="pr2 vuz3 (Pos (Succ vuz400))",fontsize=16,color="black",shape="box"];22 -> 26[label="",style="solid", color="black", weight=3];
23[label="fromInt (Pos (Succ Zero))",fontsize=16,color="black",shape="triangle"];23 -> 27[label="",style="solid", color="black", weight=3];
24[label="pr2 vuz3 (Neg (Succ vuz400))",fontsize=16,color="black",shape="box"];24 -> 28[label="",style="solid", color="black", weight=3];
25 -> 23[label="",style="dashed", color="red", weight=0];
25[label="fromInt (Pos (Succ Zero))",fontsize=16,color="magenta"];26[label="pr2Pr1 vuz3 (Pos (Succ vuz400)) (Pos (Succ vuz400) > fromInt (Pos Zero))",fontsize=16,color="black",shape="box"];26 -> 29[label="",style="solid", color="black", weight=3];
27[label="primIntToFloat (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];27 -> 30[label="",style="solid", color="black", weight=3];
28[label="pr2Pr1 vuz3 (Neg (Succ vuz400)) (Neg (Succ vuz400) > fromInt (Pos Zero))",fontsize=16,color="black",shape="box"];28 -> 31[label="",style="solid", color="black", weight=3];
29[label="pr2Pr1 vuz3 (Pos (Succ vuz400)) (compare (Pos (Succ vuz400)) (fromInt (Pos Zero)) == GT)",fontsize=16,color="black",shape="box"];29 -> 32[label="",style="solid", color="black", weight=3];
30[label="Float (Pos (Succ Zero)) (Pos (Succ Zero))",fontsize=16,color="green",shape="box"];31[label="pr2Pr1 vuz3 (Neg (Succ vuz400)) (compare (Neg (Succ vuz400)) (fromInt (Pos Zero)) == GT)",fontsize=16,color="black",shape="box"];31 -> 33[label="",style="solid", color="black", weight=3];
32[label="pr2Pr1 vuz3 (Pos (Succ vuz400)) (primCmpInt (Pos (Succ vuz400)) (fromInt (Pos Zero)) == GT)",fontsize=16,color="black",shape="box"];32 -> 34[label="",style="solid", color="black", weight=3];
33[label="pr2Pr1 vuz3 (Neg (Succ vuz400)) (primCmpInt (Neg (Succ vuz400)) (fromInt (Pos Zero)) == GT)",fontsize=16,color="black",shape="box"];33 -> 35[label="",style="solid", color="black", weight=3];
34[label="pr2Pr1 vuz3 (Pos (Succ vuz400)) (primCmpInt (Pos (Succ vuz400)) (Pos Zero) == GT)",fontsize=16,color="black",shape="box"];34 -> 36[label="",style="solid", color="black", weight=3];
35[label="pr2Pr1 vuz3 (Neg (Succ vuz400)) (primCmpInt (Neg (Succ vuz400)) (Pos Zero) == GT)",fontsize=16,color="black",shape="box"];35 -> 37[label="",style="solid", color="black", weight=3];
36[label="pr2Pr1 vuz3 (Pos (Succ vuz400)) (primCmpNat (Succ vuz400) Zero == GT)",fontsize=16,color="black",shape="box"];36 -> 38[label="",style="solid", color="black", weight=3];
37[label="pr2Pr1 vuz3 (Neg (Succ vuz400)) (LT == GT)",fontsize=16,color="black",shape="box"];37 -> 39[label="",style="solid", color="black", weight=3];
38[label="pr2Pr1 vuz3 (Pos (Succ vuz400)) (GT == GT)",fontsize=16,color="black",shape="box"];38 -> 40[label="",style="solid", color="black", weight=3];
39[label="pr2Pr1 vuz3 (Neg (Succ vuz400)) False",fontsize=16,color="black",shape="box"];39 -> 41[label="",style="solid", color="black", weight=3];
40[label="pr2Pr1 vuz3 (Pos (Succ vuz400)) True",fontsize=16,color="black",shape="box"];40 -> 42[label="",style="solid", color="black", weight=3];
41[label="pr0 vuz3 (Neg (Succ vuz400))",fontsize=16,color="black",shape="box"];41 -> 43[label="",style="solid", color="black", weight=3];
42[label="pr2F vuz3 (Pos (Succ vuz400) - fromInt (Pos (Succ Zero))) vuz3",fontsize=16,color="black",shape="box"];42 -> 44[label="",style="solid", color="black", weight=3];
43[label="error []",fontsize=16,color="black",shape="box"];43 -> 45[label="",style="solid", color="black", weight=3];
44[label="pr2F4 vuz3 (Pos (Succ vuz400) - fromInt (Pos (Succ Zero))) vuz3",fontsize=16,color="black",shape="box"];44 -> 46[label="",style="solid", color="black", weight=3];
45[label="error []",fontsize=16,color="red",shape="box"];46[label="pr2F3 (Pos (Succ vuz400) - fromInt (Pos (Succ Zero)) == fromInt (Pos Zero)) vuz3 (Pos (Succ vuz400) - fromInt (Pos (Succ Zero))) vuz3",fontsize=16,color="black",shape="box"];46 -> 47[label="",style="solid", color="black", weight=3];
47[label="pr2F3 (primEqInt (Pos (Succ vuz400) - fromInt (Pos (Succ Zero))) (fromInt (Pos Zero))) vuz3 (Pos (Succ vuz400) - fromInt (Pos (Succ Zero))) vuz3",fontsize=16,color="black",shape="box"];47 -> 48[label="",style="solid", color="black", weight=3];
48[label="pr2F3 (primEqInt (primMinusInt (Pos (Succ vuz400)) (fromInt (Pos (Succ Zero)))) (fromInt (Pos Zero))) vuz3 (primMinusInt (Pos (Succ vuz400)) (fromInt (Pos (Succ Zero)))) vuz3",fontsize=16,color="black",shape="box"];48 -> 49[label="",style="solid", color="black", weight=3];
49[label="pr2F3 (primEqInt (primMinusInt (Pos (Succ vuz400)) (Pos (Succ Zero))) (fromInt (Pos Zero))) vuz3 (primMinusInt (Pos (Succ vuz400)) (Pos (Succ Zero))) vuz3",fontsize=16,color="black",shape="box"];49 -> 50[label="",style="solid", color="black", weight=3];
50[label="pr2F3 (primEqInt (primMinusNat (Succ vuz400) (Succ Zero)) (fromInt (Pos Zero))) vuz3 (primMinusNat (Succ vuz400) (Succ Zero)) vuz3",fontsize=16,color="black",shape="box"];50 -> 51[label="",style="solid", color="black", weight=3];
51[label="pr2F3 (primEqInt (primMinusNat vuz400 Zero) (fromInt (Pos Zero))) vuz3 (primMinusNat vuz400 Zero) vuz3",fontsize=16,color="burlywood",shape="box"];1968[label="vuz400/Succ vuz4000",fontsize=10,color="white",style="solid",shape="box"];51 -> 1968[label="",style="solid", color="burlywood", weight=9];
1968 -> 52[label="",style="solid", color="burlywood", weight=3];
1969[label="vuz400/Zero",fontsize=10,color="white",style="solid",shape="box"];51 -> 1969[label="",style="solid", color="burlywood", weight=9];
1969 -> 53[label="",style="solid", color="burlywood", weight=3];
52[label="pr2F3 (primEqInt (primMinusNat (Succ vuz4000) Zero) (fromInt (Pos Zero))) vuz3 (primMinusNat (Succ vuz4000) Zero) vuz3",fontsize=16,color="black",shape="box"];52 -> 54[label="",style="solid", color="black", weight=3];
53[label="pr2F3 (primEqInt (primMinusNat Zero Zero) (fromInt (Pos Zero))) vuz3 (primMinusNat Zero Zero) vuz3",fontsize=16,color="black",shape="box"];53 -> 55[label="",style="solid", color="black", weight=3];
54[label="pr2F3 (primEqInt (Pos (Succ vuz4000)) (fromInt (Pos Zero))) vuz3 (Pos (Succ vuz4000)) vuz3",fontsize=16,color="black",shape="box"];54 -> 56[label="",style="solid", color="black", weight=3];
55[label="pr2F3 (primEqInt (Pos Zero) (fromInt (Pos Zero))) vuz3 (Pos Zero) vuz3",fontsize=16,color="black",shape="box"];55 -> 57[label="",style="solid", color="black", weight=3];
56[label="pr2F3 (primEqInt (Pos (Succ vuz4000)) (Pos Zero)) vuz3 (Pos (Succ vuz4000)) vuz3",fontsize=16,color="black",shape="box"];56 -> 58[label="",style="solid", color="black", weight=3];
57[label="pr2F3 (primEqInt (Pos Zero) (Pos Zero)) vuz3 (Pos Zero) vuz3",fontsize=16,color="black",shape="box"];57 -> 59[label="",style="solid", color="black", weight=3];
58[label="pr2F3 False vuz3 (Pos (Succ vuz4000)) vuz3",fontsize=16,color="black",shape="box"];58 -> 60[label="",style="solid", color="black", weight=3];
59[label="pr2F3 True vuz3 (Pos Zero) vuz3",fontsize=16,color="black",shape="box"];59 -> 61[label="",style="solid", color="black", weight=3];
60[label="pr2F0 vuz3 (Pos (Succ vuz4000)) vuz3",fontsize=16,color="black",shape="box"];60 -> 62[label="",style="solid", color="black", weight=3];
61[label="vuz3",fontsize=16,color="green",shape="box"];62[label="pr2F0G vuz3 vuz3 (Pos (Succ vuz4000))",fontsize=16,color="black",shape="box"];62 -> 63[label="",style="solid", color="black", weight=3];
63[label="pr2F0G2 vuz3 vuz3 (Pos (Succ vuz4000))",fontsize=16,color="black",shape="box"];63 -> 64[label="",style="solid", color="black", weight=3];
64[label="pr2F0G1 vuz3 vuz3 (Pos (Succ vuz4000)) (even (Pos (Succ vuz4000)))",fontsize=16,color="black",shape="box"];64 -> 65[label="",style="solid", color="black", weight=3];
65[label="pr2F0G1 vuz3 vuz3 (Pos (Succ vuz4000)) (primEvenInt (Pos (Succ vuz4000)))",fontsize=16,color="black",shape="box"];65 -> 66[label="",style="solid", color="black", weight=3];
66 -> 99[label="",style="dashed", color="red", weight=0];
66[label="pr2F0G1 vuz3 vuz3 (Pos (Succ vuz4000)) (primEvenNat (Succ vuz4000))",fontsize=16,color="magenta"];66 -> 100[label="",style="dashed", color="magenta", weight=3];
66 -> 101[label="",style="dashed", color="magenta", weight=3];
66 -> 102[label="",style="dashed", color="magenta", weight=3];
100[label="vuz3",fontsize=16,color="green",shape="box"];101[label="vuz4000",fontsize=16,color="green",shape="box"];102[label="Succ vuz4000",fontsize=16,color="green",shape="box"];99[label="pr2F0G1 vuz6 vuz6 (Pos (Succ vuz7)) (primEvenNat vuz8)\n  Num a",fontsize=16,color="burlywood",shape="triangle"];1971[label="vuz8/Succ vuz80",fontsize=10,color="white",style="solid",shape="box"];99 -> 1971[label="",style="solid", color="burlywood", weight=9];
1971 -> 112[label="",style="solid", color="burlywood", weight=3];
1972[label="vuz8/Zero",fontsize=10,color="white",style="solid",shape="box"];99 -> 1972[label="",style="solid", color="burlywood", weight=9];
1972 -> 113[label="",style="solid", color="burlywood", weight=3];
112[label="pr2F0G1 vuz6 vuz6 (Pos (Succ vuz7)) (primEvenNat (Succ vuz80))\n  Num a",fontsize=16,color="burlywood",shape="box"];1973[label="vuz80/Succ vuz800",fontsize=10,color="white",style="solid",shape="box"];112 -> 1973[label="",style="solid", color="burlywood", weight=9];
1973 -> 114[label="",style="solid", color="burlywood", weight=3];
1974[label="vuz80/Zero",fontsize=10,color="white",style="solid",shape="box"];112 -> 1974[label="",style="solid", color="burlywood", weight=9];
1974 -> 115[label="",style="solid", color="burlywood", weight=3];
113[label="pr2F0G1 vuz6 vuz6 (Pos (Succ vuz7)) (primEvenNat Zero)\n  Num a",fontsize=16,color="black",shape="box"];113 -> 116[label="",style="solid", color="black", weight=3];
114[label="pr2F0G1 vuz6 vuz6 (Pos (Succ vuz7)) (primEvenNat (Succ (Succ vuz800)))\n  Num a",fontsize=16,color="black",shape="box"];114 -> 117[label="",style="solid", color="black", weight=3];
115[label="pr2F0G1 vuz6 vuz6 (Pos (Succ vuz7)) (primEvenNat (Succ Zero))\n  Num a",fontsize=16,color="black",shape="box"];115 -> 118[label="",style="solid", color="black", weight=3];
116[label="pr2F0G1 vuz6 vuz6 (Pos (Succ vuz7)) True\n  Num a",fontsize=16,color="black",shape="box"];116 -> 119[label="",style="solid", color="black", weight=3];
117 -> 99[label="",style="dashed", color="red", weight=0];
117[label="pr2F0G1 vuz6 vuz6 (Pos (Succ vuz7)) (primEvenNat vuz800)\n  Num a",fontsize=16,color="magenta"];117 -> 120[label="",style="dashed", color="magenta", weight=3];
118[label="pr2F0G1 vuz6 vuz6 (Pos (Succ vuz7)) False\n  Num a",fontsize=16,color="black",shape="box"];118 -> 121[label="",style="solid", color="black", weight=3];
119[label="pr2F0G vuz6 (vuz6 * vuz6) (Pos (Succ vuz7) `quot` fromInt (Pos (Succ (Succ Zero))))\n  Num a",fontsize=16,color="black",shape="box"];119 -> 122[label="",style="solid", color="black", weight=3];
120[label="vuz800",fontsize=16,color="green",shape="box"];121[label="pr2F0G0 vuz6 vuz6 (Pos (Succ vuz7)) otherwise\n  Num a",fontsize=16,color="black",shape="box"];121 -> 123[label="",style="solid", color="black", weight=3];
122[label="pr2F0G2 vuz6 (vuz6 * vuz6) (Pos (Succ vuz7) `quot` fromInt (Pos (Succ (Succ Zero))))\n  Num a",fontsize=16,color="black",shape="box"];122 -> 124[label="",style="solid", color="black", weight=3];
123[label="pr2F0G0 vuz6 vuz6 (Pos (Succ vuz7)) True\n  Num a",fontsize=16,color="black",shape="box"];123 -> 125[label="",style="solid", color="black", weight=3];
124[label="pr2F0G1 vuz6 (vuz6 * vuz6) (Pos (Succ vuz7) `quot` fromInt (Pos (Succ (Succ Zero)))) (even (Pos (Succ vuz7) `quot` fromInt (Pos (Succ (Succ Zero)))))\n  Num a",fontsize=16,color="black",shape="box"];124 -> 126[label="",style="solid", color="black", weight=3];
125[label="pr2F vuz6 (Pos (Succ vuz7) - fromInt (Pos (Succ Zero))) (vuz6 * vuz6)\n  Num a",fontsize=16,color="black",shape="box"];125 -> 127[label="",style="solid", color="black", weight=3];
126[label="pr2F0G1 vuz6 (vuz6 * vuz6) (Pos (Succ vuz7) `quot` fromInt (Pos (Succ (Succ Zero)))) (primEvenInt (Pos (Succ vuz7) `quot` fromInt (Pos (Succ (Succ Zero)))))\n  Num a",fontsize=16,color="black",shape="box"];126 -> 128[label="",style="solid", color="black", weight=3];
127[label="pr2F4 vuz6 (Pos (Succ vuz7) - fromInt (Pos (Succ Zero))) (vuz6 * vuz6)\n  Num a",fontsize=16,color="black",shape="box"];127 -> 129[label="",style="solid", color="black", weight=3];
128 -> 901[label="",style="dashed", color="red", weight=0];
128[label="pr2F0G1 vuz6 (vuz6 * vuz6) (primQuotInt (Pos (Succ vuz7)) (fromInt (Pos (Succ (Succ Zero))))) (primEvenInt (primQuotInt (Pos (Succ vuz7)) (fromInt (Pos (Succ (Succ Zero))))))\n  Num a",fontsize=16,color="magenta"];128 -> 902[label="",style="dashed", color="magenta", weight=3];
128 -> 903[label="",style="dashed", color="magenta", weight=3];
128 -> 904[label="",style="dashed", color="magenta", weight=3];
129[label="pr2F3 (Pos (Succ vuz7) - fromInt (Pos (Succ Zero)) == fromInt (Pos Zero)) vuz6 (Pos (Succ vuz7) - fromInt (Pos (Succ Zero))) (vuz6 * vuz6)\n  Num a",fontsize=16,color="black",shape="box"];129 -> 131[label="",style="solid", color="black", weight=3];
902[label="Succ vuz7",fontsize=16,color="green",shape="box"];903[label="vuz6\n  Num a",fontsize=16,color="green",shape="box"];904[label="vuz6\n  Num a",fontsize=16,color="green",shape="box"];901[label="pr2F0G1 vuz52 (vuz53 * vuz53) (primQuotInt (Pos vuz54) (fromInt (Pos (Succ (Succ Zero))))) (primEvenInt (primQuotInt (Pos vuz54) (fromInt (Pos (Succ (Succ Zero))))))\n  Num a",fontsize=16,color="black",shape="triangle"];901 -> 920[label="",style="solid", color="black", weight=3];
131 -> 1791[label="",style="dashed", color="red", weight=0];
131[label="pr2F3 (primEqInt (Pos (Succ vuz7) - fromInt (Pos (Succ Zero))) (fromInt (Pos Zero))) vuz6 (Pos (Succ vuz7) - fromInt (Pos (Succ Zero))) (vuz6 * vuz6)\n  Num a",fontsize=16,color="magenta"];131 -> 1792[label="",style="dashed", color="magenta", weight=3];
131 -> 1793[label="",style="dashed", color="magenta", weight=3];
131 -> 1794[label="",style="dashed", color="magenta", weight=3];
920[label="pr2F0G1 vuz52 (vuz53 * vuz53) (primQuotInt (Pos vuz54) (Pos (Succ (Succ Zero)))) (primEvenInt (primQuotInt (Pos vuz54) (Pos (Succ (Succ Zero)))))\n  Num a",fontsize=16,color="black",shape="box"];920 -> 931[label="",style="solid", color="black", weight=3];
1792[label="vuz7",fontsize=16,color="green",shape="box"];1793[label="vuz6\n  Num a",fontsize=16,color="green",shape="box"];1794[label="vuz6\n  Num a",fontsize=16,color="green",shape="box"];1791[label="pr2F3 (primEqInt (Pos (Succ vuz84) - fromInt (Pos (Succ Zero))) (fromInt (Pos Zero))) vuz85 (Pos (Succ vuz84) - fromInt (Pos (Succ Zero))) (vuz85 * vuz86)\n  Num a",fontsize=16,color="black",shape="triangle"];1791 -> 1813[label="",style="solid", color="black", weight=3];
931[label="pr2F0G1 vuz52 (vuz53 * vuz53) (Pos (primDivNatS vuz54 (Succ (Succ Zero)))) (primEvenInt (Pos (primDivNatS vuz54 (Succ (Succ Zero)))))\n  Num a",fontsize=16,color="black",shape="box"];931 -> 943[label="",style="solid", color="black", weight=3];
1813[label="pr2F3 (primEqInt (primMinusInt (Pos (Succ vuz84)) (fromInt (Pos (Succ Zero)))) (fromInt (Pos Zero))) vuz85 (primMinusInt (Pos (Succ vuz84)) (fromInt (Pos (Succ Zero)))) (vuz85 * vuz86)\n  Num a",fontsize=16,color="black",shape="box"];1813 -> 1819[label="",style="solid", color="black", weight=3];
943[label="pr2F0G1 vuz52 (vuz53 * vuz53) (Pos (primDivNatS vuz54 (Succ (Succ Zero)))) (primEvenNat (primDivNatS vuz54 (Succ (Succ Zero))))\n  Num a",fontsize=16,color="burlywood",shape="box"];1978[label="vuz54/Succ vuz540",fontsize=10,color="white",style="solid",shape="box"];943 -> 1978[label="",style="solid", color="burlywood", weight=9];
1978 -> 953[label="",style="solid", color="burlywood", weight=3];
1979[label="vuz54/Zero",fontsize=10,color="white",style="solid",shape="box"];943 -> 1979[label="",style="solid", color="burlywood", weight=9];
1979 -> 954[label="",style="solid", color="burlywood", weight=3];
1819[label="pr2F3 (primEqInt (primMinusInt (Pos (Succ vuz84)) (Pos (Succ Zero))) (fromInt (Pos Zero))) vuz85 (primMinusInt (Pos (Succ vuz84)) (Pos (Succ Zero))) (vuz85 * vuz86)\n  Num a",fontsize=16,color="black",shape="box"];1819 -> 1825[label="",style="solid", color="black", weight=3];
953[label="pr2F0G1 vuz52 (vuz53 * vuz53) (Pos (primDivNatS (Succ vuz540) (Succ (Succ Zero)))) (primEvenNat (primDivNatS (Succ vuz540) (Succ (Succ Zero))))\n  Num a",fontsize=16,color="black",shape="box"];953 -> 965[label="",style="solid", color="black", weight=3];
954[label="pr2F0G1 vuz52 (vuz53 * vuz53) (Pos (primDivNatS Zero (Succ (Succ Zero)))) (primEvenNat (primDivNatS Zero (Succ (Succ Zero))))\n  Num a",fontsize=16,color="black",shape="box"];954 -> 966[label="",style="solid", color="black", weight=3];
1825[label="pr2F3 (primEqInt (primMinusNat (Succ vuz84) (Succ Zero)) (fromInt (Pos Zero))) vuz85 (primMinusNat (Succ vuz84) (Succ Zero)) (vuz85 * vuz86)\n  Num a",fontsize=16,color="black",shape="box"];1825 -> 1826[label="",style="solid", color="black", weight=3];
965[label="pr2F0G1 vuz52 (vuz53 * vuz53) (Pos (primDivNatS0 vuz540 (Succ Zero) (primGEqNatS vuz540 (Succ Zero)))) (primEvenNat (primDivNatS0 vuz540 (Succ Zero) (primGEqNatS vuz540 (Succ Zero))))\n  Num a",fontsize=16,color="burlywood",shape="box"];1980[label="vuz540/Succ vuz5400",fontsize=10,color="white",style="solid",shape="box"];965 -> 1980[label="",style="solid", color="burlywood", weight=9];
1980 -> 974[label="",style="solid", color="burlywood", weight=3];
1981[label="vuz540/Zero",fontsize=10,color="white",style="solid",shape="box"];965 -> 1981[label="",style="solid", color="burlywood", weight=9];
1981 -> 975[label="",style="solid", color="burlywood", weight=3];
966[label="pr2F0G1 vuz52 (vuz53 * vuz53) (Pos Zero) (primEvenNat Zero)\n  Num a",fontsize=16,color="black",shape="triangle"];966 -> 976[label="",style="solid", color="black", weight=3];
1826[label="pr2F3 (primEqInt (primMinusNat vuz84 Zero) (fromInt (Pos Zero))) vuz85 (primMinusNat vuz84 Zero) (vuz85 * vuz86)\n  Num a",fontsize=16,color="burlywood",shape="box"];1982[label="vuz84/Succ vuz840",fontsize=10,color="white",style="solid",shape="box"];1826 -> 1982[label="",style="solid", color="burlywood", weight=9];
1982 -> 1827[label="",style="solid", color="burlywood", weight=3];
1983[label="vuz84/Zero",fontsize=10,color="white",style="solid",shape="box"];1826 -> 1983[label="",style="solid", color="burlywood", weight=9];
1983 -> 1828[label="",style="solid", color="burlywood", weight=3];
974[label="pr2F0G1 vuz52 (vuz53 * vuz53) (Pos (primDivNatS0 (Succ vuz5400) (Succ Zero) (primGEqNatS (Succ vuz5400) (Succ Zero)))) (primEvenNat (primDivNatS0 (Succ vuz5400) (Succ Zero) (primGEqNatS (Succ vuz5400) (Succ Zero))))\n  Num a",fontsize=16,color="black",shape="box"];974 -> 992[label="",style="solid", color="black", weight=3];
975[label="pr2F0G1 vuz52 (vuz53 * vuz53) (Pos (primDivNatS0 Zero (Succ Zero) (primGEqNatS Zero (Succ Zero)))) (primEvenNat (primDivNatS0 Zero (Succ Zero) (primGEqNatS Zero (Succ Zero))))\n  Num a",fontsize=16,color="black",shape="box"];975 -> 993[label="",style="solid", color="black", weight=3];
976[label="pr2F0G1 vuz52 (vuz53 * vuz53) (Pos Zero) True\n  Num a",fontsize=16,color="black",shape="box"];976 -> 994[label="",style="solid", color="black", weight=3];
1827[label="pr2F3 (primEqInt (primMinusNat (Succ vuz840) Zero) (fromInt (Pos Zero))) vuz85 (primMinusNat (Succ vuz840) Zero) (vuz85 * vuz86)\n  Num a",fontsize=16,color="black",shape="box"];1827 -> 1829[label="",style="solid", color="black", weight=3];
1828[label="pr2F3 (primEqInt (primMinusNat Zero Zero) (fromInt (Pos Zero))) vuz85 (primMinusNat Zero Zero) (vuz85 * vuz86)\n  Num a",fontsize=16,color="black",shape="box"];1828 -> 1830[label="",style="solid", color="black", weight=3];
992[label="pr2F0G1 vuz52 (vuz53 * vuz53) (Pos (primDivNatS0 (Succ vuz5400) (Succ Zero) (primGEqNatS vuz5400 Zero))) (primEvenNat (primDivNatS0 (Succ vuz5400) (Succ Zero) (primGEqNatS vuz5400 Zero)))\n  Num a",fontsize=16,color="burlywood",shape="box"];1984[label="vuz5400/Succ vuz54000",fontsize=10,color="white",style="solid",shape="box"];992 -> 1984[label="",style="solid", color="burlywood", weight=9];
1984 -> 997[label="",style="solid", color="burlywood", weight=3];
1985[label="vuz5400/Zero",fontsize=10,color="white",style="solid",shape="box"];992 -> 1985[label="",style="solid", color="burlywood", weight=9];
1985 -> 998[label="",style="solid", color="burlywood", weight=3];
993[label="pr2F0G1 vuz52 (vuz53 * vuz53) (Pos (primDivNatS0 Zero (Succ Zero) False)) (primEvenNat (primDivNatS0 Zero (Succ Zero) False))\n  Num a",fontsize=16,color="black",shape="box"];993 -> 999[label="",style="solid", color="black", weight=3];
994[label="pr2F0G vuz52 (vuz53 * vuz53 * (vuz53 * vuz53)) (Pos Zero `quot` fromInt (Pos (Succ (Succ Zero))))\n  Num a",fontsize=16,color="black",shape="box"];994 -> 1000[label="",style="solid", color="black", weight=3];
1829[label="pr2F3 (primEqInt (Pos (Succ vuz840)) (fromInt (Pos Zero))) vuz85 (Pos (Succ vuz840)) (vuz85 * vuz86)\n  Num a",fontsize=16,color="black",shape="box"];1829 -> 1831[label="",style="solid", color="black", weight=3];
1830[label="pr2F3 (primEqInt (Pos Zero) (fromInt (Pos Zero))) vuz85 (Pos Zero) (vuz85 * vuz86)\n  Num a",fontsize=16,color="black",shape="box"];1830 -> 1832[label="",style="solid", color="black", weight=3];
997[label="pr2F0G1 vuz52 (vuz53 * vuz53) (Pos (primDivNatS0 (Succ (Succ vuz54000)) (Succ Zero) (primGEqNatS (Succ vuz54000) Zero))) (primEvenNat (primDivNatS0 (Succ (Succ vuz54000)) (Succ Zero) (primGEqNatS (Succ vuz54000) Zero)))\n  Num a",fontsize=16,color="black",shape="box"];997 -> 1004[label="",style="solid", color="black", weight=3];
998[label="pr2F0G1 vuz52 (vuz53 * vuz53) (Pos (primDivNatS0 (Succ Zero) (Succ Zero) (primGEqNatS Zero Zero))) (primEvenNat (primDivNatS0 (Succ Zero) (Succ Zero) (primGEqNatS Zero Zero)))\n  Num a",fontsize=16,color="black",shape="box"];998 -> 1005[label="",style="solid", color="black", weight=3];
999 -> 966[label="",style="dashed", color="red", weight=0];
999[label="pr2F0G1 vuz52 (vuz53 * vuz53) (Pos Zero) (primEvenNat Zero)\n  Num a",fontsize=16,color="magenta"];1000[label="pr2F0G2 vuz52 (vuz53 * vuz53 * (vuz53 * vuz53)) (Pos Zero `quot` fromInt (Pos (Succ (Succ Zero))))\n  Num a",fontsize=16,color="black",shape="box"];1000 -> 1006[label="",style="solid", color="black", weight=3];
1831[label="pr2F3 (primEqInt (Pos (Succ vuz840)) (Pos Zero)) vuz85 (Pos (Succ vuz840)) (vuz85 * vuz86)\n  Num a",fontsize=16,color="black",shape="box"];1831 -> 1833[label="",style="solid", color="black", weight=3];
1832[label="pr2F3 (primEqInt (Pos Zero) (Pos Zero)) vuz85 (Pos Zero) (vuz85 * vuz86)\n  Num a",fontsize=16,color="black",shape="box"];1832 -> 1834[label="",style="solid", color="black", weight=3];
1004[label="pr2F0G1 vuz52 (vuz53 * vuz53) (Pos (primDivNatS0 (Succ (Succ vuz54000)) (Succ Zero) True)) (primEvenNat (primDivNatS0 (Succ (Succ vuz54000)) (Succ Zero) True))\n  Num a",fontsize=16,color="black",shape="box"];1004 -> 1010[label="",style="solid", color="black", weight=3];
1005[label="pr2F0G1 vuz52 (vuz53 * vuz53) (Pos (primDivNatS0 (Succ Zero) (Succ Zero) True)) (primEvenNat (primDivNatS0 (Succ Zero) (Succ Zero) True))\n  Num a",fontsize=16,color="black",shape="box"];1005 -> 1011[label="",style="solid", color="black", weight=3];
1006[label="pr2F0G1 vuz52 (vuz53 * vuz53 * (vuz53 * vuz53)) (Pos Zero `quot` fromInt (Pos (Succ (Succ Zero)))) (even (Pos Zero `quot` fromInt (Pos (Succ (Succ Zero)))))\n  Num a",fontsize=16,color="black",shape="box"];1006 -> 1012[label="",style="solid", color="black", weight=3];
1833[label="pr2F3 False vuz85 (Pos (Succ vuz840)) (vuz85 * vuz86)\n  Num a",fontsize=16,color="black",shape="box"];1833 -> 1835[label="",style="solid", color="black", weight=3];
1834[label="pr2F3 True vuz85 (Pos Zero) (vuz85 * vuz86)\n  Num a",fontsize=16,color="black",shape="box"];1834 -> 1836[label="",style="solid", color="black", weight=3];
1010 -> 1211[label="",style="dashed", color="red", weight=0];
1010[label="pr2F0G1 vuz52 (vuz53 * vuz53) (Pos (Succ (primDivNatS (primMinusNatS (Succ (Succ vuz54000)) (Succ Zero)) (Succ (Succ Zero))))) (primEvenNat (Succ (primDivNatS (primMinusNatS (Succ (Succ vuz54000)) (Succ Zero)) (Succ (Succ Zero)))))\n  Num a",fontsize=16,color="magenta"];1010 -> 1212[label="",style="dashed", color="magenta", weight=3];
1010 -> 1213[label="",style="dashed", color="magenta", weight=3];
1010 -> 1214[label="",style="dashed", color="magenta", weight=3];
1010 -> 1215[label="",style="dashed", color="magenta", weight=3];
1011 -> 1211[label="",style="dashed", color="red", weight=0];
1011[label="pr2F0G1 vuz52 (vuz53 * vuz53) (Pos (Succ (primDivNatS (primMinusNatS (Succ Zero) (Succ Zero)) (Succ (Succ Zero))))) (primEvenNat (Succ (primDivNatS (primMinusNatS (Succ Zero) (Succ Zero)) (Succ (Succ Zero)))))\n  Num a",fontsize=16,color="magenta"];1011 -> 1216[label="",style="dashed", color="magenta", weight=3];
1011 -> 1217[label="",style="dashed", color="magenta", weight=3];
1011 -> 1218[label="",style="dashed", color="magenta", weight=3];
1011 -> 1219[label="",style="dashed", color="magenta", weight=3];
1012[label="pr2F0G1 vuz52 (vuz53 * vuz53 * (vuz53 * vuz53)) (Pos Zero `quot` fromInt (Pos (Succ (Succ Zero)))) (primEvenInt (Pos Zero `quot` fromInt (Pos (Succ (Succ Zero)))))\n  Num a",fontsize=16,color="black",shape="box"];1012 -> 1018[label="",style="solid", color="black", weight=3];
1835[label="pr2F0 vuz85 (Pos (Succ vuz840)) (vuz85 * vuz86)\n  Num a",fontsize=16,color="black",shape="box"];1835 -> 1837[label="",style="solid", color="black", weight=3];
1836[label="vuz85 * vuz86\n  Num a",fontsize=16,color="blue",shape="box"];1989[label="* :: (Ratio a) -> (Ratio a) -> Ratio a",fontsize=10,color="white",style="solid",shape="box"];1836 -> 1989[label="",style="solid", color="blue", weight=9];
1989 -> 1838[label="",style="solid", color="blue", weight=3];
1990[label="* :: Integer -> Integer -> Integer",fontsize=10,color="white",style="solid",shape="box"];1836 -> 1990[label="",style="solid", color="blue", weight=9];
1990 -> 1839[label="",style="solid", color="blue", weight=3];
1991[label="* :: Float -> Float -> Float",fontsize=10,color="white",style="solid",shape="box"];1836 -> 1991[label="",style="solid", color="blue", weight=9];
1991 -> 1840[label="",style="solid", color="blue", weight=3];
1992[label="* :: Int -> Int -> Int",fontsize=10,color="white",style="solid",shape="box"];1836 -> 1992[label="",style="solid", color="blue", weight=9];
1992 -> 1841[label="",style="solid", color="blue", weight=3];
1993[label="* :: Double -> Double -> Double",fontsize=10,color="white",style="solid",shape="box"];1836 -> 1993[label="",style="solid", color="blue", weight=9];
1993 -> 1842[label="",style="solid", color="blue", weight=3];
1212[label="vuz53\n  Num a",fontsize=16,color="green",shape="box"];1213[label="primDivNatS (primMinusNatS (Succ (Succ vuz54000)) (Succ Zero)) (Succ (Succ Zero))",fontsize=16,color="black",shape="triangle"];1213 -> 1236[label="",style="solid", color="black", weight=3];
1214[label="Succ (primDivNatS (primMinusNatS (Succ (Succ vuz54000)) (Succ Zero)) (Succ (Succ Zero)))",fontsize=16,color="green",shape="box"];1214 -> 1237[label="",style="dashed", color="green", weight=3];
1215[label="vuz52\n  Num a",fontsize=16,color="green",shape="box"];1211[label="pr2F0G1 vuz64 (vuz65 * vuz65) (Pos (Succ vuz66)) (primEvenNat vuz67)\n  Num a",fontsize=16,color="burlywood",shape="triangle"];1994[label="vuz67/Succ vuz670",fontsize=10,color="white",style="solid",shape="box"];1211 -> 1994[label="",style="solid", color="burlywood", weight=9];
1994 -> 1238[label="",style="solid", color="burlywood", weight=3];
1995[label="vuz67/Zero",fontsize=10,color="white",style="solid",shape="box"];1211 -> 1995[label="",style="solid", color="burlywood", weight=9];
1995 -> 1239[label="",style="solid", color="burlywood", weight=3];
1216[label="vuz53\n  Num a",fontsize=16,color="green",shape="box"];1217[label="primDivNatS (primMinusNatS (Succ Zero) (Succ Zero)) (Succ (Succ Zero))",fontsize=16,color="black",shape="triangle"];1217 -> 1240[label="",style="solid", color="black", weight=3];
1218[label="Succ (primDivNatS (primMinusNatS (Succ Zero) (Succ Zero)) (Succ (Succ Zero)))",fontsize=16,color="green",shape="box"];1218 -> 1241[label="",style="dashed", color="green", weight=3];
1219[label="vuz52\n  Num a",fontsize=16,color="green",shape="box"];1018 -> 901[label="",style="dashed", color="red", weight=0];
1018[label="pr2F0G1 vuz52 (vuz53 * vuz53 * (vuz53 * vuz53)) (primQuotInt (Pos Zero) (fromInt (Pos (Succ (Succ Zero))))) (primEvenInt (primQuotInt (Pos Zero) (fromInt (Pos (Succ (Succ Zero))))))\n  Num a",fontsize=16,color="magenta"];1018 -> 1023[label="",style="dashed", color="magenta", weight=3];
1018 -> 1024[label="",style="dashed", color="magenta", weight=3];
1837[label="pr2F0G (vuz85 * vuz86) vuz85 (Pos (Succ vuz840))\n  Num a",fontsize=16,color="black",shape="box"];1837 -> 1843[label="",style="solid", color="black", weight=3];
1838 -> 684[label="",style="dashed", color="red", weight=0];
1838[label="vuz85 * vuz86\n  Integral a",fontsize=16,color="magenta"];1838 -> 1844[label="",style="dashed", color="magenta", weight=3];
1838 -> 1845[label="",style="dashed", color="magenta", weight=3];
1839 -> 696[label="",style="dashed", color="red", weight=0];
1839[label="vuz85 * vuz86",fontsize=16,color="magenta"];1839 -> 1846[label="",style="dashed", color="magenta", weight=3];
1839 -> 1847[label="",style="dashed", color="magenta", weight=3];
1840 -> 705[label="",style="dashed", color="red", weight=0];
1840[label="vuz85 * vuz86",fontsize=16,color="magenta"];1840 -> 1848[label="",style="dashed", color="magenta", weight=3];
1840 -> 1849[label="",style="dashed", color="magenta", weight=3];
1841 -> 715[label="",style="dashed", color="red", weight=0];
1841[label="vuz85 * vuz86",fontsize=16,color="magenta"];1841 -> 1850[label="",style="dashed", color="magenta", weight=3];
1841 -> 1851[label="",style="dashed", color="magenta", weight=3];
1842 -> 726[label="",style="dashed", color="red", weight=0];
1842[label="vuz85 * vuz86",fontsize=16,color="magenta"];1842 -> 1852[label="",style="dashed", color="magenta", weight=3];
1842 -> 1853[label="",style="dashed", color="magenta", weight=3];
1236[label="primDivNatS (primMinusNatS (Succ vuz54000) Zero) (Succ (Succ Zero))",fontsize=16,color="black",shape="box"];1236 -> 1253[label="",style="solid", color="black", weight=3];
1237 -> 1213[label="",style="dashed", color="red", weight=0];
1237[label="primDivNatS (primMinusNatS (Succ (Succ vuz54000)) (Succ Zero)) (Succ (Succ Zero))",fontsize=16,color="magenta"];1238[label="pr2F0G1 vuz64 (vuz65 * vuz65) (Pos (Succ vuz66)) (primEvenNat (Succ vuz670))\n  Num a",fontsize=16,color="burlywood",shape="box"];2003[label="vuz670/Succ vuz6700",fontsize=10,color="white",style="solid",shape="box"];1238 -> 2003[label="",style="solid", color="burlywood", weight=9];
2003 -> 1254[label="",style="solid", color="burlywood", weight=3];
2004[label="vuz670/Zero",fontsize=10,color="white",style="solid",shape="box"];1238 -> 2004[label="",style="solid", color="burlywood", weight=9];
2004 -> 1255[label="",style="solid", color="burlywood", weight=3];
1239[label="pr2F0G1 vuz64 (vuz65 * vuz65) (Pos (Succ vuz66)) (primEvenNat Zero)\n  Num a",fontsize=16,color="black",shape="box"];1239 -> 1256[label="",style="solid", color="black", weight=3];
1240[label="primDivNatS (primMinusNatS Zero Zero) (Succ (Succ Zero))",fontsize=16,color="black",shape="box"];1240 -> 1257[label="",style="solid", color="black", weight=3];
1241 -> 1217[label="",style="dashed", color="red", weight=0];
1241[label="primDivNatS (primMinusNatS (Succ Zero) (Succ Zero)) (Succ (Succ Zero))",fontsize=16,color="magenta"];1023[label="Zero",fontsize=16,color="green",shape="box"];1024[label="vuz53 * vuz53\n  Num a",fontsize=16,color="blue",shape="box"];2006[label="* :: (Ratio a) -> (Ratio a) -> Ratio a",fontsize=10,color="white",style="solid",shape="box"];1024 -> 2006[label="",style="solid", color="blue", weight=9];
2006 -> 1029[label="",style="solid", color="blue", weight=3];
2007[label="* :: Integer -> Integer -> Integer",fontsize=10,color="white",style="solid",shape="box"];1024 -> 2007[label="",style="solid", color="blue", weight=9];
2007 -> 1030[label="",style="solid", color="blue", weight=3];
2008[label="* :: Float -> Float -> Float",fontsize=10,color="white",style="solid",shape="box"];1024 -> 2008[label="",style="solid", color="blue", weight=9];
2008 -> 1031[label="",style="solid", color="blue", weight=3];
2009[label="* :: Int -> Int -> Int",fontsize=10,color="white",style="solid",shape="box"];1024 -> 2009[label="",style="solid", color="blue", weight=9];
2009 -> 1032[label="",style="solid", color="blue", weight=3];
2010[label="* :: Double -> Double -> Double",fontsize=10,color="white",style="solid",shape="box"];1024 -> 2010[label="",style="solid", color="blue", weight=9];
2010 -> 1033[label="",style="solid", color="blue", weight=3];
1843[label="pr2F0G2 (vuz85 * vuz86) vuz85 (Pos (Succ vuz840))\n  Num a",fontsize=16,color="black",shape="box"];1843 -> 1854[label="",style="solid", color="black", weight=3];
1844[label="vuz86\n  Integral a",fontsize=16,color="green",shape="box"];1845[label="vuz85\n  Integral a",fontsize=16,color="green",shape="box"];684[label="vuz13 * vuz37\n  Integral a",fontsize=16,color="black",shape="triangle"];684 -> 690[label="",style="solid", color="black", weight=3];
1846[label="vuz85",fontsize=16,color="green",shape="box"];1847[label="vuz86",fontsize=16,color="green",shape="box"];696[label="vuz38 * vuz17",fontsize=16,color="black",shape="triangle"];696 -> 702[label="",style="solid", color="black", weight=3];
1848[label="vuz86",fontsize=16,color="green",shape="box"];1849[label="vuz85",fontsize=16,color="green",shape="box"];705[label="vuz39 * vuz17",fontsize=16,color="black",shape="triangle"];705 -> 711[label="",style="solid", color="black", weight=3];
1850[label="vuz85",fontsize=16,color="green",shape="box"];1851[label="vuz86",fontsize=16,color="green",shape="box"];715[label="vuz40 * vuz17",fontsize=16,color="black",shape="triangle"];715 -> 721[label="",style="solid", color="black", weight=3];
1852[label="vuz86",fontsize=16,color="green",shape="box"];1853[label="vuz85",fontsize=16,color="green",shape="box"];726[label="vuz41 * vuz17",fontsize=16,color="black",shape="triangle"];726 -> 732[label="",style="solid", color="black", weight=3];
1253[label="primDivNatS (Succ vuz54000) (Succ (Succ Zero))",fontsize=16,color="black",shape="box"];1253 -> 1264[label="",style="solid", color="black", weight=3];
1254[label="pr2F0G1 vuz64 (vuz65 * vuz65) (Pos (Succ vuz66)) (primEvenNat (Succ (Succ vuz6700)))\n  Num a",fontsize=16,color="black",shape="box"];1254 -> 1265[label="",style="solid", color="black", weight=3];
1255[label="pr2F0G1 vuz64 (vuz65 * vuz65) (Pos (Succ vuz66)) (primEvenNat (Succ Zero))\n  Num a",fontsize=16,color="black",shape="box"];1255 -> 1266[label="",style="solid", color="black", weight=3];
1256[label="pr2F0G1 vuz64 (vuz65 * vuz65) (Pos (Succ vuz66)) True\n  Num a",fontsize=16,color="black",shape="box"];1256 -> 1267[label="",style="solid", color="black", weight=3];
1257[label="primDivNatS Zero (Succ (Succ Zero))",fontsize=16,color="black",shape="box"];1257 -> 1268[label="",style="solid", color="black", weight=3];
1029 -> 169[label="",style="dashed", color="red", weight=0];
1029[label="vuz53 * vuz53\n  Integral a",fontsize=16,color="magenta"];1029 -> 1039[label="",style="dashed", color="magenta", weight=3];
1030 -> 170[label="",style="dashed", color="red", weight=0];
1030[label="vuz53 * vuz53",fontsize=16,color="magenta"];1030 -> 1040[label="",style="dashed", color="magenta", weight=3];
1031 -> 171[label="",style="dashed", color="red", weight=0];
1031[label="vuz53 * vuz53",fontsize=16,color="magenta"];1031 -> 1041[label="",style="dashed", color="magenta", weight=3];
1032 -> 172[label="",style="dashed", color="red", weight=0];
1032[label="vuz53 * vuz53",fontsize=16,color="magenta"];1032 -> 1042[label="",style="dashed", color="magenta", weight=3];
1033 -> 173[label="",style="dashed", color="red", weight=0];
1033[label="vuz53 * vuz53",fontsize=16,color="magenta"];1033 -> 1043[label="",style="dashed", color="magenta", weight=3];
1854[label="pr2F0G1 (vuz85 * vuz86) vuz85 (Pos (Succ vuz840)) (even (Pos (Succ vuz840)))\n  Num a",fontsize=16,color="black",shape="box"];1854 -> 1855[label="",style="solid", color="black", weight=3];
690[label="error []",fontsize=16,color="red",shape="box"];702[label="error []",fontsize=16,color="red",shape="box"];711[label="primMulFloat vuz39 vuz17",fontsize=16,color="burlywood",shape="box"];2016[label="vuz39/Float vuz390 vuz391",fontsize=10,color="white",style="solid",shape="box"];711 -> 2016[label="",style="solid", color="burlywood", weight=9];
2016 -> 722[label="",style="solid", color="burlywood", weight=3];
721[label="primMulInt vuz40 vuz17",fontsize=16,color="burlywood",shape="box"];2017[label="vuz40/Pos vuz400",fontsize=10,color="white",style="solid",shape="box"];721 -> 2017[label="",style="solid", color="burlywood", weight=9];
2017 -> 733[label="",style="solid", color="burlywood", weight=3];
2018[label="vuz40/Neg vuz400",fontsize=10,color="white",style="solid",shape="box"];721 -> 2018[label="",style="solid", color="burlywood", weight=9];
2018 -> 734[label="",style="solid", color="burlywood", weight=3];
732[label="error []",fontsize=16,color="red",shape="box"];1264[label="primDivNatS0 vuz54000 (Succ Zero) (primGEqNatS vuz54000 (Succ Zero))",fontsize=16,color="burlywood",shape="box"];2019[label="vuz54000/Succ vuz540000",fontsize=10,color="white",style="solid",shape="box"];1264 -> 2019[label="",style="solid", color="burlywood", weight=9];
2019 -> 1270[label="",style="solid", color="burlywood", weight=3];
2020[label="vuz54000/Zero",fontsize=10,color="white",style="solid",shape="box"];1264 -> 2020[label="",style="solid", color="burlywood", weight=9];
2020 -> 1271[label="",style="solid", color="burlywood", weight=3];
1265 -> 1211[label="",style="dashed", color="red", weight=0];
1265[label="pr2F0G1 vuz64 (vuz65 * vuz65) (Pos (Succ vuz66)) (primEvenNat vuz6700)\n  Num a",fontsize=16,color="magenta"];1265 -> 1272[label="",style="dashed", color="magenta", weight=3];
1266[label="pr2F0G1 vuz64 (vuz65 * vuz65) (Pos (Succ vuz66)) False\n  Num a",fontsize=16,color="black",shape="box"];1266 -> 1273[label="",style="solid", color="black", weight=3];
1267[label="pr2F0G vuz64 (vuz65 * vuz65 * (vuz65 * vuz65)) (Pos (Succ vuz66) `quot` fromInt (Pos (Succ (Succ Zero))))\n  Num a",fontsize=16,color="black",shape="box"];1267 -> 1274[label="",style="solid", color="black", weight=3];
1268[label="Zero",fontsize=16,color="green",shape="box"];1039[label="vuz53\n  Integral a",fontsize=16,color="green",shape="box"];169 -> 684[label="",style="dashed", color="red", weight=0];
169[label="vuz6 * vuz6\n  Integral a",fontsize=16,color="magenta"];169 -> 685[label="",style="dashed", color="magenta", weight=3];
169 -> 686[label="",style="dashed", color="magenta", weight=3];
1040[label="vuz53",fontsize=16,color="green",shape="box"];170 -> 696[label="",style="dashed", color="red", weight=0];
170[label="vuz6 * vuz6",fontsize=16,color="magenta"];170 -> 697[label="",style="dashed", color="magenta", weight=3];
170 -> 698[label="",style="dashed", color="magenta", weight=3];
1041[label="vuz53",fontsize=16,color="green",shape="box"];171 -> 705[label="",style="dashed", color="red", weight=0];
171[label="vuz6 * vuz6",fontsize=16,color="magenta"];171 -> 706[label="",style="dashed", color="magenta", weight=3];
171 -> 707[label="",style="dashed", color="magenta", weight=3];
1042[label="vuz53",fontsize=16,color="green",shape="box"];172 -> 715[label="",style="dashed", color="red", weight=0];
172[label="vuz6 * vuz6",fontsize=16,color="magenta"];172 -> 716[label="",style="dashed", color="magenta", weight=3];
172 -> 717[label="",style="dashed", color="magenta", weight=3];
1043[label="vuz53",fontsize=16,color="green",shape="box"];173 -> 726[label="",style="dashed", color="red", weight=0];
173[label="vuz6 * vuz6",fontsize=16,color="magenta"];173 -> 727[label="",style="dashed", color="magenta", weight=3];
173 -> 728[label="",style="dashed", color="magenta", weight=3];
1855[label="pr2F0G1 (vuz85 * vuz86) vuz85 (Pos (Succ vuz840)) (primEvenInt (Pos (Succ vuz840)))\n  Num a",fontsize=16,color="black",shape="box"];1855 -> 1856[label="",style="solid", color="black", weight=3];
722[label="primMulFloat (Float vuz390 vuz391) vuz17",fontsize=16,color="burlywood",shape="box"];2027[label="vuz17/Float vuz170 vuz171",fontsize=10,color="white",style="solid",shape="box"];722 -> 2027[label="",style="solid", color="burlywood", weight=9];
2027 -> 735[label="",style="solid", color="burlywood", weight=3];
733[label="primMulInt (Pos vuz400) vuz17",fontsize=16,color="burlywood",shape="box"];2028[label="vuz17/Pos vuz170",fontsize=10,color="white",style="solid",shape="box"];733 -> 2028[label="",style="solid", color="burlywood", weight=9];
2028 -> 745[label="",style="solid", color="burlywood", weight=3];
2029[label="vuz17/Neg vuz170",fontsize=10,color="white",style="solid",shape="box"];733 -> 2029[label="",style="solid", color="burlywood", weight=9];
2029 -> 746[label="",style="solid", color="burlywood", weight=3];
734[label="primMulInt (Neg vuz400) vuz17",fontsize=16,color="burlywood",shape="box"];2030[label="vuz17/Pos vuz170",fontsize=10,color="white",style="solid",shape="box"];734 -> 2030[label="",style="solid", color="burlywood", weight=9];
2030 -> 747[label="",style="solid", color="burlywood", weight=3];
2031[label="vuz17/Neg vuz170",fontsize=10,color="white",style="solid",shape="box"];734 -> 2031[label="",style="solid", color="burlywood", weight=9];
2031 -> 748[label="",style="solid", color="burlywood", weight=3];
1270[label="primDivNatS0 (Succ vuz540000) (Succ Zero) (primGEqNatS (Succ vuz540000) (Succ Zero))",fontsize=16,color="black",shape="box"];1270 -> 1277[label="",style="solid", color="black", weight=3];
1271[label="primDivNatS0 Zero (Succ Zero) (primGEqNatS Zero (Succ Zero))",fontsize=16,color="black",shape="box"];1271 -> 1278[label="",style="solid", color="black", weight=3];
1272[label="vuz6700",fontsize=16,color="green",shape="box"];1273[label="pr2F0G0 vuz64 (vuz65 * vuz65) (Pos (Succ vuz66)) otherwise\n  Num a",fontsize=16,color="black",shape="box"];1273 -> 1279[label="",style="solid", color="black", weight=3];
1274[label="pr2F0G2 vuz64 (vuz65 * vuz65 * (vuz65 * vuz65)) (Pos (Succ vuz66) `quot` fromInt (Pos (Succ (Succ Zero))))\n  Num a",fontsize=16,color="black",shape="box"];1274 -> 1280[label="",style="solid", color="black", weight=3];
685[label="vuz6\n  Integral a",fontsize=16,color="green",shape="box"];686[label="vuz6\n  Integral a",fontsize=16,color="green",shape="box"];697[label="vuz6",fontsize=16,color="green",shape="box"];698[label="vuz6",fontsize=16,color="green",shape="box"];706[label="vuz6",fontsize=16,color="green",shape="box"];707[label="vuz6",fontsize=16,color="green",shape="box"];716[label="vuz6",fontsize=16,color="green",shape="box"];717[label="vuz6",fontsize=16,color="green",shape="box"];727[label="vuz6",fontsize=16,color="green",shape="box"];728[label="vuz6",fontsize=16,color="green",shape="box"];1856 -> 1889[label="",style="dashed", color="red", weight=0];
1856[label="pr2F0G1 (vuz85 * vuz86) vuz85 (Pos (Succ vuz840)) (primEvenNat (Succ vuz840))\n  Num a",fontsize=16,color="magenta"];1856 -> 1890[label="",style="dashed", color="magenta", weight=3];
1856 -> 1891[label="",style="dashed", color="magenta", weight=3];
1856 -> 1892[label="",style="dashed", color="magenta", weight=3];
1856 -> 1893[label="",style="dashed", color="magenta", weight=3];
735[label="primMulFloat (Float vuz390 vuz391) (Float vuz170 vuz171)",fontsize=16,color="black",shape="box"];735 -> 749[label="",style="solid", color="black", weight=3];
745[label="primMulInt (Pos vuz400) (Pos vuz170)",fontsize=16,color="black",shape="box"];745 -> 770[label="",style="solid", color="black", weight=3];
746[label="primMulInt (Pos vuz400) (Neg vuz170)",fontsize=16,color="black",shape="box"];746 -> 771[label="",style="solid", color="black", weight=3];
747[label="primMulInt (Neg vuz400) (Pos vuz170)",fontsize=16,color="black",shape="box"];747 -> 772[label="",style="solid", color="black", weight=3];
748[label="primMulInt (Neg vuz400) (Neg vuz170)",fontsize=16,color="black",shape="box"];748 -> 773[label="",style="solid", color="black", weight=3];
1277[label="primDivNatS0 (Succ vuz540000) (Succ Zero) (primGEqNatS vuz540000 Zero)",fontsize=16,color="burlywood",shape="box"];2033[label="vuz540000/Succ vuz5400000",fontsize=10,color="white",style="solid",shape="box"];1277 -> 2033[label="",style="solid", color="burlywood", weight=9];
2033 -> 1283[label="",style="solid", color="burlywood", weight=3];
2034[label="vuz540000/Zero",fontsize=10,color="white",style="solid",shape="box"];1277 -> 2034[label="",style="solid", color="burlywood", weight=9];
2034 -> 1284[label="",style="solid", color="burlywood", weight=3];
1278[label="primDivNatS0 Zero (Succ Zero) False",fontsize=16,color="black",shape="box"];1278 -> 1285[label="",style="solid", color="black", weight=3];
1279[label="pr2F0G0 vuz64 (vuz65 * vuz65) (Pos (Succ vuz66)) True\n  Num a",fontsize=16,color="black",shape="box"];1279 -> 1286[label="",style="solid", color="black", weight=3];
1280[label="pr2F0G1 vuz64 (vuz65 * vuz65 * (vuz65 * vuz65)) (Pos (Succ vuz66) `quot` fromInt (Pos (Succ (Succ Zero)))) (even (Pos (Succ vuz66) `quot` fromInt (Pos (Succ (Succ Zero)))))\n  Num a",fontsize=16,color="black",shape="box"];1280 -> 1287[label="",style="solid", color="black", weight=3];
1890[label="vuz85\n  Num a",fontsize=16,color="green",shape="box"];1891[label="vuz86\n  Num a",fontsize=16,color="green",shape="box"];1892[label="Succ vuz840",fontsize=16,color="green",shape="box"];1893[label="vuz840",fontsize=16,color="green",shape="box"];1889[label="pr2F0G1 (vuz88 * vuz89) vuz88 (Pos (Succ vuz90)) (primEvenNat vuz91)\n  Num a",fontsize=16,color="burlywood",shape="triangle"];2035[label="vuz91/Succ vuz910",fontsize=10,color="white",style="solid",shape="box"];1889 -> 2035[label="",style="solid", color="burlywood", weight=9];
2035 -> 1906[label="",style="solid", color="burlywood", weight=3];
2036[label="vuz91/Zero",fontsize=10,color="white",style="solid",shape="box"];1889 -> 2036[label="",style="solid", color="burlywood", weight=9];
2036 -> 1907[label="",style="solid", color="burlywood", weight=3];
749[label="Float (vuz390 * vuz170) (vuz391 * vuz171)",fontsize=16,color="green",shape="box"];749 -> 774[label="",style="dashed", color="green", weight=3];
749 -> 775[label="",style="dashed", color="green", weight=3];
770[label="Pos (primMulNat vuz400 vuz170)",fontsize=16,color="green",shape="box"];770 -> 789[label="",style="dashed", color="green", weight=3];
771[label="Neg (primMulNat vuz400 vuz170)",fontsize=16,color="green",shape="box"];771 -> 790[label="",style="dashed", color="green", weight=3];
772[label="Neg (primMulNat vuz400 vuz170)",fontsize=16,color="green",shape="box"];772 -> 791[label="",style="dashed", color="green", weight=3];
773[label="Pos (primMulNat vuz400 vuz170)",fontsize=16,color="green",shape="box"];773 -> 792[label="",style="dashed", color="green", weight=3];
1283[label="primDivNatS0 (Succ (Succ vuz5400000)) (Succ Zero) (primGEqNatS (Succ vuz5400000) Zero)",fontsize=16,color="black",shape="box"];1283 -> 1291[label="",style="solid", color="black", weight=3];
1284[label="primDivNatS0 (Succ Zero) (Succ Zero) (primGEqNatS Zero Zero)",fontsize=16,color="black",shape="box"];1284 -> 1292[label="",style="solid", color="black", weight=3];
1285[label="Zero",fontsize=16,color="green",shape="box"];1286[label="pr2F (vuz65 * vuz65) (Pos (Succ vuz66) - fromInt (Pos (Succ Zero))) (vuz65 * vuz65 * vuz64)\n  Num a",fontsize=16,color="black",shape="box"];1286 -> 1293[label="",style="solid", color="black", weight=3];
1287[label="pr2F0G1 vuz64 (vuz65 * vuz65 * (vuz65 * vuz65)) (Pos (Succ vuz66) `quot` fromInt (Pos (Succ (Succ Zero)))) (primEvenInt (Pos (Succ vuz66) `quot` fromInt (Pos (Succ (Succ Zero)))))\n  Num a",fontsize=16,color="black",shape="box"];1287 -> 1294[label="",style="solid", color="black", weight=3];
1906[label="pr2F0G1 (vuz88 * vuz89) vuz88 (Pos (Succ vuz90)) (primEvenNat (Succ vuz910))\n  Num a",fontsize=16,color="burlywood",shape="box"];2037[label="vuz910/Succ vuz9100",fontsize=10,color="white",style="solid",shape="box"];1906 -> 2037[label="",style="solid", color="burlywood", weight=9];
2037 -> 1908[label="",style="solid", color="burlywood", weight=3];
2038[label="vuz910/Zero",fontsize=10,color="white",style="solid",shape="box"];1906 -> 2038[label="",style="solid", color="burlywood", weight=9];
2038 -> 1909[label="",style="solid", color="burlywood", weight=3];
1907[label="pr2F0G1 (vuz88 * vuz89) vuz88 (Pos (Succ vuz90)) (primEvenNat Zero)\n  Num a",fontsize=16,color="black",shape="box"];1907 -> 1910[label="",style="solid", color="black", weight=3];
774 -> 715[label="",style="dashed", color="red", weight=0];
774[label="vuz390 * vuz170",fontsize=16,color="magenta"];774 -> 793[label="",style="dashed", color="magenta", weight=3];
774 -> 794[label="",style="dashed", color="magenta", weight=3];
775 -> 715[label="",style="dashed", color="red", weight=0];
775[label="vuz391 * vuz171",fontsize=16,color="magenta"];775 -> 795[label="",style="dashed", color="magenta", weight=3];
775 -> 796[label="",style="dashed", color="magenta", weight=3];
789[label="primMulNat vuz400 vuz170",fontsize=16,color="burlywood",shape="triangle"];2041[label="vuz400/Succ vuz4000",fontsize=10,color="white",style="solid",shape="box"];789 -> 2041[label="",style="solid", color="burlywood", weight=9];
2041 -> 810[label="",style="solid", color="burlywood", weight=3];
2042[label="vuz400/Zero",fontsize=10,color="white",style="solid",shape="box"];789 -> 2042[label="",style="solid", color="burlywood", weight=9];
2042 -> 811[label="",style="solid", color="burlywood", weight=3];
790 -> 789[label="",style="dashed", color="red", weight=0];
790[label="primMulNat vuz400 vuz170",fontsize=16,color="magenta"];790 -> 812[label="",style="dashed", color="magenta", weight=3];
791 -> 789[label="",style="dashed", color="red", weight=0];
791[label="primMulNat vuz400 vuz170",fontsize=16,color="magenta"];791 -> 813[label="",style="dashed", color="magenta", weight=3];
792 -> 789[label="",style="dashed", color="red", weight=0];
792[label="primMulNat vuz400 vuz170",fontsize=16,color="magenta"];792 -> 814[label="",style="dashed", color="magenta", weight=3];
792 -> 815[label="",style="dashed", color="magenta", weight=3];
1291[label="primDivNatS0 (Succ (Succ vuz5400000)) (Succ Zero) True",fontsize=16,color="black",shape="box"];1291 -> 1299[label="",style="solid", color="black", weight=3];
1292[label="primDivNatS0 (Succ Zero) (Succ Zero) True",fontsize=16,color="black",shape="box"];1292 -> 1300[label="",style="solid", color="black", weight=3];
1293[label="pr2F4 (vuz65 * vuz65) (Pos (Succ vuz66) - fromInt (Pos (Succ Zero))) (vuz65 * vuz65 * vuz64)\n  Num a",fontsize=16,color="black",shape="box"];1293 -> 1301[label="",style="solid", color="black", weight=3];
1294 -> 901[label="",style="dashed", color="red", weight=0];
1294[label="pr2F0G1 vuz64 (vuz65 * vuz65 * (vuz65 * vuz65)) (primQuotInt (Pos (Succ vuz66)) (fromInt (Pos (Succ (Succ Zero))))) (primEvenInt (primQuotInt (Pos (Succ vuz66)) (fromInt (Pos (Succ (Succ Zero))))))\n  Num a",fontsize=16,color="magenta"];1294 -> 1302[label="",style="dashed", color="magenta", weight=3];
1294 -> 1303[label="",style="dashed", color="magenta", weight=3];
1294 -> 1304[label="",style="dashed", color="magenta", weight=3];
1908[label="pr2F0G1 (vuz88 * vuz89) vuz88 (Pos (Succ vuz90)) (primEvenNat (Succ (Succ vuz9100)))\n  Num a",fontsize=16,color="black",shape="box"];1908 -> 1911[label="",style="solid", color="black", weight=3];
1909[label="pr2F0G1 (vuz88 * vuz89) vuz88 (Pos (Succ vuz90)) (primEvenNat (Succ Zero))\n  Num a",fontsize=16,color="black",shape="box"];1909 -> 1912[label="",style="solid", color="black", weight=3];
1910[label="pr2F0G1 (vuz88 * vuz89) vuz88 (Pos (Succ vuz90)) True\n  Num a",fontsize=16,color="black",shape="box"];1910 -> 1913[label="",style="solid", color="black", weight=3];
793[label="vuz390",fontsize=16,color="green",shape="box"];794[label="vuz170",fontsize=16,color="green",shape="box"];795[label="vuz391",fontsize=16,color="green",shape="box"];796[label="vuz171",fontsize=16,color="green",shape="box"];810[label="primMulNat (Succ vuz4000) vuz170",fontsize=16,color="burlywood",shape="box"];2047[label="vuz170/Succ vuz1700",fontsize=10,color="white",style="solid",shape="box"];810 -> 2047[label="",style="solid", color="burlywood", weight=9];
2047 -> 828[label="",style="solid", color="burlywood", weight=3];
2048[label="vuz170/Zero",fontsize=10,color="white",style="solid",shape="box"];810 -> 2048[label="",style="solid", color="burlywood", weight=9];
2048 -> 829[label="",style="solid", color="burlywood", weight=3];
811[label="primMulNat Zero vuz170",fontsize=16,color="burlywood",shape="box"];2049[label="vuz170/Succ vuz1700",fontsize=10,color="white",style="solid",shape="box"];811 -> 2049[label="",style="solid", color="burlywood", weight=9];
2049 -> 830[label="",style="solid", color="burlywood", weight=3];
2050[label="vuz170/Zero",fontsize=10,color="white",style="solid",shape="box"];811 -> 2050[label="",style="solid", color="burlywood", weight=9];
2050 -> 831[label="",style="solid", color="burlywood", weight=3];
812[label="vuz170",fontsize=16,color="green",shape="box"];813[label="vuz400",fontsize=16,color="green",shape="box"];814[label="vuz170",fontsize=16,color="green",shape="box"];815[label="vuz400",fontsize=16,color="green",shape="box"];1299[label="Succ (primDivNatS (primMinusNatS (Succ (Succ vuz5400000)) (Succ Zero)) (Succ (Succ Zero)))",fontsize=16,color="green",shape="box"];1299 -> 1309[label="",style="dashed", color="green", weight=3];
1300[label="Succ (primDivNatS (primMinusNatS (Succ Zero) (Succ Zero)) (Succ (Succ Zero)))",fontsize=16,color="green",shape="box"];1300 -> 1310[label="",style="dashed", color="green", weight=3];
1301[label="pr2F3 (Pos (Succ vuz66) - fromInt (Pos (Succ Zero)) == fromInt (Pos Zero)) (vuz65 * vuz65) (Pos (Succ vuz66) - fromInt (Pos (Succ Zero))) (vuz65 * vuz65 * vuz64)\n  Num a",fontsize=16,color="black",shape="box"];1301 -> 1311[label="",style="solid", color="black", weight=3];
1302[label="Succ vuz66",fontsize=16,color="green",shape="box"];1303[label="vuz64\n  Num a",fontsize=16,color="green",shape="box"];1304[label="vuz65 * vuz65\n  Num a",fontsize=16,color="blue",shape="box"];2051[label="* :: (Ratio a) -> (Ratio a) -> Ratio a",fontsize=10,color="white",style="solid",shape="box"];1304 -> 2051[label="",style="solid", color="blue", weight=9];
2051 -> 1312[label="",style="solid", color="blue", weight=3];
2052[label="* :: Integer -> Integer -> Integer",fontsize=10,color="white",style="solid",shape="box"];1304 -> 2052[label="",style="solid", color="blue", weight=9];
2052 -> 1313[label="",style="solid", color="blue", weight=3];
2053[label="* :: Float -> Float -> Float",fontsize=10,color="white",style="solid",shape="box"];1304 -> 2053[label="",style="solid", color="blue", weight=9];
2053 -> 1314[label="",style="solid", color="blue", weight=3];
2054[label="* :: Int -> Int -> Int",fontsize=10,color="white",style="solid",shape="box"];1304 -> 2054[label="",style="solid", color="blue", weight=9];
2054 -> 1315[label="",style="solid", color="blue", weight=3];
2055[label="* :: Double -> Double -> Double",fontsize=10,color="white",style="solid",shape="box"];1304 -> 2055[label="",style="solid", color="blue", weight=9];
2055 -> 1316[label="",style="solid", color="blue", weight=3];
1911 -> 1889[label="",style="dashed", color="red", weight=0];
1911[label="pr2F0G1 (vuz88 * vuz89) vuz88 (Pos (Succ vuz90)) (primEvenNat vuz9100)\n  Num a",fontsize=16,color="magenta"];1911 -> 1914[label="",style="dashed", color="magenta", weight=3];
1912[label="pr2F0G1 (vuz88 * vuz89) vuz88 (Pos (Succ vuz90)) False\n  Num a",fontsize=16,color="black",shape="box"];1912 -> 1915[label="",style="solid", color="black", weight=3];
1913[label="pr2F0G (vuz88 * vuz89) (vuz88 * vuz88) (Pos (Succ vuz90) `quot` fromInt (Pos (Succ (Succ Zero))))\n  Num a",fontsize=16,color="black",shape="box"];1913 -> 1916[label="",style="solid", color="black", weight=3];
828[label="primMulNat (Succ vuz4000) (Succ vuz1700)",fontsize=16,color="black",shape="box"];828 -> 846[label="",style="solid", color="black", weight=3];
829[label="primMulNat (Succ vuz4000) Zero",fontsize=16,color="black",shape="box"];829 -> 847[label="",style="solid", color="black", weight=3];
830[label="primMulNat Zero (Succ vuz1700)",fontsize=16,color="black",shape="box"];830 -> 848[label="",style="solid", color="black", weight=3];
831[label="primMulNat Zero Zero",fontsize=16,color="black",shape="box"];831 -> 849[label="",style="solid", color="black", weight=3];
1309 -> 1213[label="",style="dashed", color="red", weight=0];
1309[label="primDivNatS (primMinusNatS (Succ (Succ vuz5400000)) (Succ Zero)) (Succ (Succ Zero))",fontsize=16,color="magenta"];1309 -> 1322[label="",style="dashed", color="magenta", weight=3];
1310 -> 1217[label="",style="dashed", color="red", weight=0];
1310[label="primDivNatS (primMinusNatS (Succ Zero) (Succ Zero)) (Succ (Succ Zero))",fontsize=16,color="magenta"];1311 -> 1791[label="",style="dashed", color="red", weight=0];
1311[label="pr2F3 (primEqInt (Pos (Succ vuz66) - fromInt (Pos (Succ Zero))) (fromInt (Pos Zero))) (vuz65 * vuz65) (Pos (Succ vuz66) - fromInt (Pos (Succ Zero))) (vuz65 * vuz65 * vuz64)\n  Num a",fontsize=16,color="magenta"];1311 -> 1795[label="",style="dashed", color="magenta", weight=3];
1311 -> 1796[label="",style="dashed", color="magenta", weight=3];
1311 -> 1797[label="",style="dashed", color="magenta", weight=3];
1312 -> 169[label="",style="dashed", color="red", weight=0];
1312[label="vuz65 * vuz65\n  Integral a",fontsize=16,color="magenta"];1312 -> 1324[label="",style="dashed", color="magenta", weight=3];
1313 -> 170[label="",style="dashed", color="red", weight=0];
1313[label="vuz65 * vuz65",fontsize=16,color="magenta"];1313 -> 1325[label="",style="dashed", color="magenta", weight=3];
1314 -> 171[label="",style="dashed", color="red", weight=0];
1314[label="vuz65 * vuz65",fontsize=16,color="magenta"];1314 -> 1326[label="",style="dashed", color="magenta", weight=3];
1315 -> 172[label="",style="dashed", color="red", weight=0];
1315[label="vuz65 * vuz65",fontsize=16,color="magenta"];1315 -> 1327[label="",style="dashed", color="magenta", weight=3];
1316 -> 173[label="",style="dashed", color="red", weight=0];
1316[label="vuz65 * vuz65",fontsize=16,color="magenta"];1316 -> 1328[label="",style="dashed", color="magenta", weight=3];
1914[label="vuz9100",fontsize=16,color="green",shape="box"];1915[label="pr2F0G0 (vuz88 * vuz89) vuz88 (Pos (Succ vuz90)) otherwise\n  Num a",fontsize=16,color="black",shape="box"];1915 -> 1917[label="",style="solid", color="black", weight=3];
1916[label="pr2F0G2 (vuz88 * vuz89) (vuz88 * vuz88) (Pos (Succ vuz90) `quot` fromInt (Pos (Succ (Succ Zero))))\n  Num a",fontsize=16,color="black",shape="box"];1916 -> 1918[label="",style="solid", color="black", weight=3];
846 -> 871[label="",style="dashed", color="red", weight=0];
846[label="primPlusNat (primMulNat vuz4000 (Succ vuz1700)) (Succ vuz1700)",fontsize=16,color="magenta"];846 -> 872[label="",style="dashed", color="magenta", weight=3];
847[label="Zero",fontsize=16,color="green",shape="box"];848[label="Zero",fontsize=16,color="green",shape="box"];849[label="Zero",fontsize=16,color="green",shape="box"];1322[label="vuz5400000",fontsize=16,color="green",shape="box"];1795[label="vuz66",fontsize=16,color="green",shape="box"];1796[label="vuz64\n  Num a",fontsize=16,color="green",shape="box"];1797[label="vuz65 * vuz65\n  Num a",fontsize=16,color="blue",shape="box"];2066[label="* :: (Ratio a) -> (Ratio a) -> Ratio a",fontsize=10,color="white",style="solid",shape="box"];1797 -> 2066[label="",style="solid", color="blue", weight=9];
2066 -> 1814[label="",style="solid", color="blue", weight=3];
2067[label="* :: Integer -> Integer -> Integer",fontsize=10,color="white",style="solid",shape="box"];1797 -> 2067[label="",style="solid", color="blue", weight=9];
2067 -> 1815[label="",style="solid", color="blue", weight=3];
2068[label="* :: Float -> Float -> Float",fontsize=10,color="white",style="solid",shape="box"];1797 -> 2068[label="",style="solid", color="blue", weight=9];
2068 -> 1816[label="",style="solid", color="blue", weight=3];
2069[label="* :: Int -> Int -> Int",fontsize=10,color="white",style="solid",shape="box"];1797 -> 2069[label="",style="solid", color="blue", weight=9];
2069 -> 1817[label="",style="solid", color="blue", weight=3];
2070[label="* :: Double -> Double -> Double",fontsize=10,color="white",style="solid",shape="box"];1797 -> 2070[label="",style="solid", color="blue", weight=9];
2070 -> 1818[label="",style="solid", color="blue", weight=3];
1324[label="vuz65\n  Integral a",fontsize=16,color="green",shape="box"];1325[label="vuz65",fontsize=16,color="green",shape="box"];1326[label="vuz65",fontsize=16,color="green",shape="box"];1327[label="vuz65",fontsize=16,color="green",shape="box"];1328[label="vuz65",fontsize=16,color="green",shape="box"];1917[label="pr2F0G0 (vuz88 * vuz89) vuz88 (Pos (Succ vuz90)) True\n  Num a",fontsize=16,color="black",shape="box"];1917 -> 1919[label="",style="solid", color="black", weight=3];
1918[label="pr2F0G1 (vuz88 * vuz89) (vuz88 * vuz88) (Pos (Succ vuz90) `quot` fromInt (Pos (Succ (Succ Zero)))) (even (Pos (Succ vuz90) `quot` fromInt (Pos (Succ (Succ Zero)))))\n  Num a",fontsize=16,color="black",shape="box"];1918 -> 1920[label="",style="solid", color="black", weight=3];
872 -> 789[label="",style="dashed", color="red", weight=0];
872[label="primMulNat vuz4000 (Succ vuz1700)",fontsize=16,color="magenta"];872 -> 873[label="",style="dashed", color="magenta", weight=3];
872 -> 874[label="",style="dashed", color="magenta", weight=3];
871[label="primPlusNat vuz50 (Succ vuz1700)",fontsize=16,color="burlywood",shape="triangle"];2072[label="vuz50/Succ vuz500",fontsize=10,color="white",style="solid",shape="box"];871 -> 2072[label="",style="solid", color="burlywood", weight=9];
2072 -> 875[label="",style="solid", color="burlywood", weight=3];
2073[label="vuz50/Zero",fontsize=10,color="white",style="solid",shape="box"];871 -> 2073[label="",style="solid", color="burlywood", weight=9];
2073 -> 876[label="",style="solid", color="burlywood", weight=3];
1814 -> 169[label="",style="dashed", color="red", weight=0];
1814[label="vuz65 * vuz65\n  Integral a",fontsize=16,color="magenta"];1814 -> 1820[label="",style="dashed", color="magenta", weight=3];
1815 -> 170[label="",style="dashed", color="red", weight=0];
1815[label="vuz65 * vuz65",fontsize=16,color="magenta"];1815 -> 1821[label="",style="dashed", color="magenta", weight=3];
1816 -> 171[label="",style="dashed", color="red", weight=0];
1816[label="vuz65 * vuz65",fontsize=16,color="magenta"];1816 -> 1822[label="",style="dashed", color="magenta", weight=3];
1817 -> 172[label="",style="dashed", color="red", weight=0];
1817[label="vuz65 * vuz65",fontsize=16,color="magenta"];1817 -> 1823[label="",style="dashed", color="magenta", weight=3];
1818 -> 173[label="",style="dashed", color="red", weight=0];
1818[label="vuz65 * vuz65",fontsize=16,color="magenta"];1818 -> 1824[label="",style="dashed", color="magenta", weight=3];
1919[label="pr2F vuz88 (Pos (Succ vuz90) - fromInt (Pos (Succ Zero))) (vuz88 * (vuz88 * vuz89))\n  Num a",fontsize=16,color="black",shape="box"];1919 -> 1921[label="",style="solid", color="black", weight=3];
1920[label="pr2F0G1 (vuz88 * vuz89) (vuz88 * vuz88) (Pos (Succ vuz90) `quot` fromInt (Pos (Succ (Succ Zero)))) (primEvenInt (Pos (Succ vuz90) `quot` fromInt (Pos (Succ (Succ Zero)))))\n  Num a",fontsize=16,color="black",shape="box"];1920 -> 1922[label="",style="solid", color="black", weight=3];
873[label="Succ vuz1700",fontsize=16,color="green",shape="box"];874[label="vuz4000",fontsize=16,color="green",shape="box"];875[label="primPlusNat (Succ vuz500) (Succ vuz1700)",fontsize=16,color="black",shape="box"];875 -> 897[label="",style="solid", color="black", weight=3];
876[label="primPlusNat Zero (Succ vuz1700)",fontsize=16,color="black",shape="box"];876 -> 898[label="",style="solid", color="black", weight=3];
1820[label="vuz65\n  Integral a",fontsize=16,color="green",shape="box"];1821[label="vuz65",fontsize=16,color="green",shape="box"];1822[label="vuz65",fontsize=16,color="green",shape="box"];1823[label="vuz65",fontsize=16,color="green",shape="box"];1824[label="vuz65",fontsize=16,color="green",shape="box"];1921[label="pr2F4 vuz88 (Pos (Succ vuz90) - fromInt (Pos (Succ Zero))) (vuz88 * (vuz88 * vuz89))\n  Num a",fontsize=16,color="black",shape="box"];1921 -> 1923[label="",style="solid", color="black", weight=3];
1922 -> 901[label="",style="dashed", color="red", weight=0];
1922[label="pr2F0G1 (vuz88 * vuz89) (vuz88 * vuz88) (primQuotInt (Pos (Succ vuz90)) (fromInt (Pos (Succ (Succ Zero))))) (primEvenInt (primQuotInt (Pos (Succ vuz90)) (fromInt (Pos (Succ (Succ Zero))))))\n  Num a",fontsize=16,color="magenta"];1922 -> 1924[label="",style="dashed", color="magenta", weight=3];
1922 -> 1925[label="",style="dashed", color="magenta", weight=3];
1922 -> 1926[label="",style="dashed", color="magenta", weight=3];
897[label="Succ (Succ (primPlusNat vuz500 vuz1700))",fontsize=16,color="green",shape="box"];897 -> 921[label="",style="dashed", color="green", weight=3];
898[label="Succ vuz1700",fontsize=16,color="green",shape="box"];1923[label="pr2F3 (Pos (Succ vuz90) - fromInt (Pos (Succ Zero)) == fromInt (Pos Zero)) vuz88 (Pos (Succ vuz90) - fromInt (Pos (Succ Zero))) (vuz88 * (vuz88 * vuz89))\n  Num a",fontsize=16,color="black",shape="box"];1923 -> 1927[label="",style="solid", color="black", weight=3];
1924[label="Succ vuz90",fontsize=16,color="green",shape="box"];1925[label="vuz88 * vuz89\n  Num a",fontsize=16,color="blue",shape="box"];2080[label="* :: (Ratio a) -> (Ratio a) -> Ratio a",fontsize=10,color="white",style="solid",shape="box"];1925 -> 2080[label="",style="solid", color="blue", weight=9];
2080 -> 1928[label="",style="solid", color="blue", weight=3];
2081[label="* :: Integer -> Integer -> Integer",fontsize=10,color="white",style="solid",shape="box"];1925 -> 2081[label="",style="solid", color="blue", weight=9];
2081 -> 1929[label="",style="solid", color="blue", weight=3];
2082[label="* :: Float -> Float -> Float",fontsize=10,color="white",style="solid",shape="box"];1925 -> 2082[label="",style="solid", color="blue", weight=9];
2082 -> 1930[label="",style="solid", color="blue", weight=3];
2083[label="* :: Int -> Int -> Int",fontsize=10,color="white",style="solid",shape="box"];1925 -> 2083[label="",style="solid", color="blue", weight=9];
2083 -> 1931[label="",style="solid", color="blue", weight=3];
2084[label="* :: Double -> Double -> Double",fontsize=10,color="white",style="solid",shape="box"];1925 -> 2084[label="",style="solid", color="blue", weight=9];
2084 -> 1932[label="",style="solid", color="blue", weight=3];
1926[label="vuz88\n  Num a",fontsize=16,color="green",shape="box"];921[label="primPlusNat vuz500 vuz1700",fontsize=16,color="burlywood",shape="triangle"];2085[label="vuz500/Succ vuz5000",fontsize=10,color="white",style="solid",shape="box"];921 -> 2085[label="",style="solid", color="burlywood", weight=9];
2085 -> 932[label="",style="solid", color="burlywood", weight=3];
2086[label="vuz500/Zero",fontsize=10,color="white",style="solid",shape="box"];921 -> 2086[label="",style="solid", color="burlywood", weight=9];
2086 -> 933[label="",style="solid", color="burlywood", weight=3];
1927 -> 1791[label="",style="dashed", color="red", weight=0];
1927[label="pr2F3 (primEqInt (Pos (Succ vuz90) - fromInt (Pos (Succ Zero))) (fromInt (Pos Zero))) vuz88 (Pos (Succ vuz90) - fromInt (Pos (Succ Zero))) (vuz88 * (vuz88 * vuz89))\n  Num a",fontsize=16,color="magenta"];1927 -> 1933[label="",style="dashed", color="magenta", weight=3];
1927 -> 1934[label="",style="dashed", color="magenta", weight=3];
1927 -> 1935[label="",style="dashed", color="magenta", weight=3];
1928 -> 684[label="",style="dashed", color="red", weight=0];
1928[label="vuz88 * vuz89\n  Integral a",fontsize=16,color="magenta"];1928 -> 1936[label="",style="dashed", color="magenta", weight=3];
1928 -> 1937[label="",style="dashed", color="magenta", weight=3];
1929 -> 696[label="",style="dashed", color="red", weight=0];
1929[label="vuz88 * vuz89",fontsize=16,color="magenta"];1929 -> 1938[label="",style="dashed", color="magenta", weight=3];
1929 -> 1939[label="",style="dashed", color="magenta", weight=3];
1930 -> 705[label="",style="dashed", color="red", weight=0];
1930[label="vuz88 * vuz89",fontsize=16,color="magenta"];1930 -> 1940[label="",style="dashed", color="magenta", weight=3];
1930 -> 1941[label="",style="dashed", color="magenta", weight=3];
1931 -> 715[label="",style="dashed", color="red", weight=0];
1931[label="vuz88 * vuz89",fontsize=16,color="magenta"];1931 -> 1942[label="",style="dashed", color="magenta", weight=3];
1931 -> 1943[label="",style="dashed", color="magenta", weight=3];
1932 -> 726[label="",style="dashed", color="red", weight=0];
1932[label="vuz88 * vuz89",fontsize=16,color="magenta"];1932 -> 1944[label="",style="dashed", color="magenta", weight=3];
1932 -> 1945[label="",style="dashed", color="magenta", weight=3];
932[label="primPlusNat (Succ vuz5000) vuz1700",fontsize=16,color="burlywood",shape="box"];2093[label="vuz1700/Succ vuz17000",fontsize=10,color="white",style="solid",shape="box"];932 -> 2093[label="",style="solid", color="burlywood", weight=9];
2093 -> 944[label="",style="solid", color="burlywood", weight=3];
2094[label="vuz1700/Zero",fontsize=10,color="white",style="solid",shape="box"];932 -> 2094[label="",style="solid", color="burlywood", weight=9];
2094 -> 945[label="",style="solid", color="burlywood", weight=3];
933[label="primPlusNat Zero vuz1700",fontsize=16,color="burlywood",shape="box"];2095[label="vuz1700/Succ vuz17000",fontsize=10,color="white",style="solid",shape="box"];933 -> 2095[label="",style="solid", color="burlywood", weight=9];
2095 -> 946[label="",style="solid", color="burlywood", weight=3];
2096[label="vuz1700/Zero",fontsize=10,color="white",style="solid",shape="box"];933 -> 2096[label="",style="solid", color="burlywood", weight=9];
2096 -> 947[label="",style="solid", color="burlywood", weight=3];
1933[label="vuz90",fontsize=16,color="green",shape="box"];1934[label="vuz88 * vuz89\n  Num a",fontsize=16,color="blue",shape="box"];2097[label="* :: (Ratio a) -> (Ratio a) -> Ratio a",fontsize=10,color="white",style="solid",shape="box"];1934 -> 2097[label="",style="solid", color="blue", weight=9];
2097 -> 1946[label="",style="solid", color="blue", weight=3];
2098[label="* :: Integer -> Integer -> Integer",fontsize=10,color="white",style="solid",shape="box"];1934 -> 2098[label="",style="solid", color="blue", weight=9];
2098 -> 1947[label="",style="solid", color="blue", weight=3];
2099[label="* :: Float -> Float -> Float",fontsize=10,color="white",style="solid",shape="box"];1934 -> 2099[label="",style="solid", color="blue", weight=9];
2099 -> 1948[label="",style="solid", color="blue", weight=3];
2100[label="* :: Int -> Int -> Int",fontsize=10,color="white",style="solid",shape="box"];1934 -> 2100[label="",style="solid", color="blue", weight=9];
2100 -> 1949[label="",style="solid", color="blue", weight=3];
2101[label="* :: Double -> Double -> Double",fontsize=10,color="white",style="solid",shape="box"];1934 -> 2101[label="",style="solid", color="blue", weight=9];
2101 -> 1950[label="",style="solid", color="blue", weight=3];
1935[label="vuz88\n  Num a",fontsize=16,color="green",shape="box"];1936[label="vuz89\n  Integral a",fontsize=16,color="green",shape="box"];1937[label="vuz88\n  Integral a",fontsize=16,color="green",shape="box"];1938[label="vuz88",fontsize=16,color="green",shape="box"];1939[label="vuz89",fontsize=16,color="green",shape="box"];1940[label="vuz89",fontsize=16,color="green",shape="box"];1941[label="vuz88",fontsize=16,color="green",shape="box"];1942[label="vuz88",fontsize=16,color="green",shape="box"];1943[label="vuz89",fontsize=16,color="green",shape="box"];1944[label="vuz89",fontsize=16,color="green",shape="box"];1945[label="vuz88",fontsize=16,color="green",shape="box"];944[label="primPlusNat (Succ vuz5000) (Succ vuz17000)",fontsize=16,color="black",shape="box"];944 -> 955[label="",style="solid", color="black", weight=3];
945[label="primPlusNat (Succ vuz5000) Zero",fontsize=16,color="black",shape="box"];945 -> 956[label="",style="solid", color="black", weight=3];
946[label="primPlusNat Zero (Succ vuz17000)",fontsize=16,color="black",shape="box"];946 -> 957[label="",style="solid", color="black", weight=3];
947[label="primPlusNat Zero Zero",fontsize=16,color="black",shape="box"];947 -> 958[label="",style="solid", color="black", weight=3];
1946 -> 684[label="",style="dashed", color="red", weight=0];
1946[label="vuz88 * vuz89\n  Integral a",fontsize=16,color="magenta"];1946 -> 1951[label="",style="dashed", color="magenta", weight=3];
1946 -> 1952[label="",style="dashed", color="magenta", weight=3];
1947 -> 696[label="",style="dashed", color="red", weight=0];
1947[label="vuz88 * vuz89",fontsize=16,color="magenta"];1947 -> 1953[label="",style="dashed", color="magenta", weight=3];
1947 -> 1954[label="",style="dashed", color="magenta", weight=3];
1948 -> 705[label="",style="dashed", color="red", weight=0];
1948[label="vuz88 * vuz89",fontsize=16,color="magenta"];1948 -> 1955[label="",style="dashed", color="magenta", weight=3];
1948 -> 1956[label="",style="dashed", color="magenta", weight=3];
1949 -> 715[label="",style="dashed", color="red", weight=0];
1949[label="vuz88 * vuz89",fontsize=16,color="magenta"];1949 -> 1957[label="",style="dashed", color="magenta", weight=3];
1949 -> 1958[label="",style="dashed", color="magenta", weight=3];
1950 -> 726[label="",style="dashed", color="red", weight=0];
1950[label="vuz88 * vuz89",fontsize=16,color="magenta"];1950 -> 1959[label="",style="dashed", color="magenta", weight=3];
1950 -> 1960[label="",style="dashed", color="magenta", weight=3];
955[label="Succ (Succ (primPlusNat vuz5000 vuz17000))",fontsize=16,color="green",shape="box"];955 -> 967[label="",style="dashed", color="green", weight=3];
956[label="Succ vuz5000",fontsize=16,color="green",shape="box"];957[label="Succ vuz17000",fontsize=16,color="green",shape="box"];958[label="Zero",fontsize=16,color="green",shape="box"];1951[label="vuz89\n  Integral a",fontsize=16,color="green",shape="box"];1952[label="vuz88\n  Integral a",fontsize=16,color="green",shape="box"];1953[label="vuz88",fontsize=16,color="green",shape="box"];1954[label="vuz89",fontsize=16,color="green",shape="box"];1955[label="vuz89",fontsize=16,color="green",shape="box"];1956[label="vuz88",fontsize=16,color="green",shape="box"];1957[label="vuz88",fontsize=16,color="green",shape="box"];1958[label="vuz89",fontsize=16,color="green",shape="box"];1959[label="vuz89",fontsize=16,color="green",shape="box"];1960[label="vuz88",fontsize=16,color="green",shape="box"];967 -> 921[label="",style="dashed", color="red", weight=0];
967[label="primPlusNat vuz5000 vuz17000",fontsize=16,color="magenta"];967 -> 977[label="",style="dashed", color="magenta", weight=3];
967 -> 978[label="",style="dashed", color="magenta", weight=3];
977[label="vuz17000",fontsize=16,color="green",shape="box"];978[label="vuz5000",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                            ↳ QDPSizeChangeProof

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS(Succ(Succ(vuz5400000))) → new_primDivNatS(vuz5400000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_primDivNatS(Succ(Succ(vuz5400000))) → new_primDivNatS(vuz5400000)
The graph contains the following edges 1 > 1

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                            ↳ QDPSizeChangeProof

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(vuz5000), Succ(vuz17000)) → new_primPlusNat(vuz5000, vuz17000)

From the DPs we obtained the following set of size-change graphs:

new_primPlusNat(Succ(vuz5000), Succ(vuz17000)) → new_primPlusNat(vuz5000, vuz17000)
The graph contains the following edges 1 > 1, 2 > 2

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ QDPSizeChangeProof

                          ↳ QDP

                          ↳ QDP

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(vuz4000), Succ(vuz1700)) → new_primMulNat(vuz4000, Succ(vuz1700))

From the DPs we obtained the following set of size-change graphs:

new_primMulNat(Succ(vuz4000), Succ(vuz1700)) → new_primMulNat(vuz4000, Succ(vuz1700))
The graph contains the following edges 1 > 1, 2 >= 2

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ DependencyGraphProof

                          ↳ QDP

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_pr2F0G1(vuz88, vuz89, vuz90, Succ(Succ(vuz9100)), ba) → new_pr2F0G1(vuz88, vuz89, vuz90, vuz9100, ba)
new_pr2F3(Succ(vuz840), vuz85, vuz86, bb) → new_pr2F0G1(vuz85, vuz86, vuz840, Succ(vuz840), bb)
new_pr2F0G12(vuz52, vuz53, bc) → new_pr2F0G10(vuz52, new_sr1(vuz53, bc), Zero, bc)
new_pr2F0G10(vuz52, vuz53, Succ(Succ(Zero)), bc) → new_pr2F0G11(vuz52, vuz53, new_primDivNatS1, Succ(new_primDivNatS1), bc)
new_pr2F0G1(vuz88, vuz89, vuz90, Succ(Zero), ba) → new_pr2F3(vuz90, vuz88, new_sr(vuz88, vuz89, ba), ba)
new_pr2F0G10(vuz52, vuz53, Succ(Succ(Succ(vuz54000))), bc) → new_pr2F0G11(vuz52, vuz53, new_primDivNatS0(vuz54000), Succ(new_primDivNatS0(vuz54000)), bc)
new_pr2F0G10(vuz52, vuz53, Zero, bc) → new_pr2F0G10(vuz52, new_sr1(vuz53, bc), Zero, bc)
new_pr2F0G11(vuz64, vuz65, vuz66, Zero, bd) → new_pr2F0G10(vuz64, new_sr3(vuz65, bd), Succ(vuz66), bd)
new_pr2F0G1(vuz88, vuz89, vuz90, Zero, ba) → new_pr2F0G10(new_sr0(vuz88, vuz89, ba), vuz88, Succ(vuz90), ba)
new_pr2F0G11(vuz64, vuz65, vuz66, Succ(Succ(vuz6700)), bd) → new_pr2F0G11(vuz64, vuz65, vuz66, vuz6700, bd)
new_pr2F0G10(vuz52, vuz53, Succ(Zero), bc) → new_pr2F0G12(vuz52, vuz53, bc)
new_pr2F0G11(vuz64, vuz65, vuz66, Succ(Zero), bd) → new_pr2F3(vuz66, new_sr2(vuz65, bd), vuz64, bd)

The TRS R consists of the following rules:

new_sr0(vuz88, vuz89, ty_Integer) → new_sr12(vuz88, vuz89)
new_sr(vuz88, vuz89, ty_Double) → new_sr10(vuz88, vuz89)
new_sr3(vuz65, ty_Float) → new_sr6(vuz65)
new_sr9(vuz13, vuz37, ca) → error([])
new_sr0(vuz88, vuz89, ty_Double) → new_sr10(vuz88, vuz89)
new_primPlusNat1(Succ(vuz5000), Succ(vuz17000)) → Succ(Succ(new_primPlusNat1(vuz5000, vuz17000)))
new_sr3(vuz65, ty_Integer) → new_sr5(vuz65)
new_primMulNat0(Succ(vuz4000), Zero) → Zero
new_primMulNat0(Zero, Succ(vuz1700)) → Zero
new_sr6(vuz6) → new_sr13(vuz6, vuz6)
new_sr1(vuz53, app(ty_Ratio, bh)) → new_sr4(vuz53, bh)
new_sr2(vuz65, ty_Integer) → new_sr5(vuz65)
new_sr2(vuz65, ty_Float) → new_sr6(vuz65)
new_primPlusNat1(Zero, Zero) → Zero
new_sr1(vuz53, ty_Float) → new_sr6(vuz53)
new_sr(vuz88, vuz89, ty_Int) → new_sr11(vuz88, vuz89)
new_sr0(vuz88, vuz89, app(ty_Ratio, bg)) → new_sr9(vuz88, vuz89, bg)
new_primDivNatS1 → Zero
new_primMulNat0(Succ(vuz4000), Succ(vuz1700)) → new_primPlusNat0(new_primMulNat0(vuz4000, Succ(vuz1700)), vuz1700)
new_sr8(vuz6) → new_sr10(vuz6, vuz6)
new_sr0(vuz88, vuz89, ty_Float) → new_sr13(vuz88, vuz89)
new_sr1(vuz53, ty_Double) → new_sr8(vuz53)
new_sr11(Pos(vuz400), Neg(vuz170)) → Neg(new_primMulNat0(vuz400, vuz170))
new_sr11(Neg(vuz400), Pos(vuz170)) → Neg(new_primMulNat0(vuz400, vuz170))
new_sr(vuz88, vuz89, app(ty_Ratio, bg)) → new_sr9(vuz88, vuz89, bg)
new_sr2(vuz65, ty_Double) → new_sr8(vuz65)
new_sr10(vuz41, vuz17) → error([])
new_primMulNat0(Zero, Zero) → Zero
new_sr2(vuz65, ty_Int) → new_sr7(vuz65)
new_sr4(vuz6, bf) → new_sr9(vuz6, vuz6, bf)
new_primPlusNat0(Succ(vuz500), vuz1700) → Succ(Succ(new_primPlusNat1(vuz500, vuz1700)))
new_sr3(vuz65, app(ty_Ratio, be)) → new_sr4(vuz65, be)
new_sr11(Neg(vuz400), Neg(vuz170)) → Pos(new_primMulNat0(vuz400, vuz170))
new_sr(vuz88, vuz89, ty_Integer) → new_sr12(vuz88, vuz89)
new_primPlusNat0(Zero, vuz1700) → Succ(vuz1700)
new_sr0(vuz88, vuz89, ty_Int) → new_sr11(vuz88, vuz89)
new_sr2(vuz65, app(ty_Ratio, be)) → new_sr4(vuz65, be)
new_primDivNatS0(Succ(Succ(vuz5400000))) → Succ(new_primDivNatS0(vuz5400000))
new_sr11(Pos(vuz400), Pos(vuz170)) → Pos(new_primMulNat0(vuz400, vuz170))
new_sr12(vuz38, vuz17) → error([])
new_sr1(vuz53, ty_Integer) → new_sr5(vuz53)
new_primDivNatS0(Succ(Zero)) → Succ(new_primDivNatS1)
new_sr3(vuz65, ty_Double) → new_sr8(vuz65)
new_sr5(vuz6) → new_sr12(vuz6, vuz6)
new_primPlusNat1(Zero, Succ(vuz17000)) → Succ(vuz17000)
new_primPlusNat1(Succ(vuz5000), Zero) → Succ(vuz5000)
new_sr(vuz88, vuz89, ty_Float) → new_sr13(vuz88, vuz89)
new_sr13(Float(vuz390, vuz391), Float(vuz170, vuz171)) → Float(new_sr11(vuz390, vuz170), new_sr11(vuz391, vuz171))
new_primDivNatS0(Zero) → Zero
new_sr3(vuz65, ty_Int) → new_sr7(vuz65)
new_sr1(vuz53, ty_Int) → new_sr7(vuz53)
new_sr7(vuz6) → new_sr11(vuz6, vuz6)

The set Q consists of the following terms:

new_sr2(x0, ty_Float)
new_sr0(x0, x1, ty_Int)
new_sr1(x0, ty_Int)
new_primPlusNat1(Succ(x0), Succ(x1))
new_primMulNat0(Succ(x0), Zero)
new_primMulNat0(Zero, Zero)
new_sr12(x0, x1)
new_sr1(x0, ty_Double)
new_primDivNatS1
new_sr3(x0, app(ty_Ratio, x1))
new_sr3(x0, ty_Float)
new_sr11(Neg(x0), Neg(x1))
new_primPlusNat1(Zero, Zero)
new_sr(x0, x1, ty_Float)
new_sr7(x0)
new_sr0(x0, x1, ty_Integer)
new_sr0(x0, x1, app(ty_Ratio, x2))
new_sr(x0, x1, ty_Int)
new_sr6(x0)
new_sr(x0, x1, ty_Double)
new_sr0(x0, x1, ty_Double)
new_sr9(x0, x1, x2)
new_sr2(x0, ty_Double)
new_sr8(x0)
new_sr(x0, x1, ty_Integer)
new_sr11(Pos(x0), Pos(x1))
new_sr3(x0, ty_Double)
new_primPlusNat1(Succ(x0), Zero)
new_sr3(x0, ty_Int)
new_sr13(Float(x0, x1), Float(x2, x3))
new_sr3(x0, ty_Integer)
new_sr1(x0, app(ty_Ratio, x1))
new_primDivNatS0(Succ(Succ(x0)))
new_sr11(Pos(x0), Neg(x1))
new_sr11(Neg(x0), Pos(x1))
new_sr2(x0, ty_Integer)
new_primDivNatS0(Zero)
new_primDivNatS0(Succ(Zero))
new_primPlusNat0(Succ(x0), x1)
new_sr1(x0, ty_Integer)
new_sr2(x0, app(ty_Ratio, x1))
new_sr4(x0, x1)
new_sr1(x0, ty_Float)
new_sr5(x0)
new_sr(x0, x1, app(ty_Ratio, x2))
new_primPlusNat1(Zero, Succ(x0))
new_primPlusNat0(Zero, x0)
new_primMulNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Succ(x0))
new_sr10(x0, x1)
new_sr0(x0, x1, ty_Float)
new_sr2(x0, ty_Int)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 2 less nodes.

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ AND

                                ↳ QDP

                                  ↳ UsableRulesProof

                                ↳ QDP

                          ↳ QDP

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_pr2F0G10(vuz52, vuz53, Zero, bc) → new_pr2F0G10(vuz52, new_sr1(vuz53, bc), Zero, bc)

The TRS R consists of the following rules:

new_sr0(vuz88, vuz89, ty_Integer) → new_sr12(vuz88, vuz89)
new_sr(vuz88, vuz89, ty_Double) → new_sr10(vuz88, vuz89)
new_sr3(vuz65, ty_Float) → new_sr6(vuz65)
new_sr9(vuz13, vuz37, ca) → error([])
new_sr0(vuz88, vuz89, ty_Double) → new_sr10(vuz88, vuz89)
new_primPlusNat1(Succ(vuz5000), Succ(vuz17000)) → Succ(Succ(new_primPlusNat1(vuz5000, vuz17000)))
new_sr3(vuz65, ty_Integer) → new_sr5(vuz65)
new_primMulNat0(Succ(vuz4000), Zero) → Zero
new_primMulNat0(Zero, Succ(vuz1700)) → Zero
new_sr6(vuz6) → new_sr13(vuz6, vuz6)
new_sr1(vuz53, app(ty_Ratio, bh)) → new_sr4(vuz53, bh)
new_sr2(vuz65, ty_Integer) → new_sr5(vuz65)
new_sr2(vuz65, ty_Float) → new_sr6(vuz65)
new_primPlusNat1(Zero, Zero) → Zero
new_sr1(vuz53, ty_Float) → new_sr6(vuz53)
new_sr(vuz88, vuz89, ty_Int) → new_sr11(vuz88, vuz89)
new_sr0(vuz88, vuz89, app(ty_Ratio, bg)) → new_sr9(vuz88, vuz89, bg)
new_primDivNatS1 → Zero
new_primMulNat0(Succ(vuz4000), Succ(vuz1700)) → new_primPlusNat0(new_primMulNat0(vuz4000, Succ(vuz1700)), vuz1700)
new_sr8(vuz6) → new_sr10(vuz6, vuz6)
new_sr0(vuz88, vuz89, ty_Float) → new_sr13(vuz88, vuz89)
new_sr1(vuz53, ty_Double) → new_sr8(vuz53)
new_sr11(Pos(vuz400), Neg(vuz170)) → Neg(new_primMulNat0(vuz400, vuz170))
new_sr11(Neg(vuz400), Pos(vuz170)) → Neg(new_primMulNat0(vuz400, vuz170))
new_sr(vuz88, vuz89, app(ty_Ratio, bg)) → new_sr9(vuz88, vuz89, bg)
new_sr2(vuz65, ty_Double) → new_sr8(vuz65)
new_sr10(vuz41, vuz17) → error([])
new_primMulNat0(Zero, Zero) → Zero
new_sr2(vuz65, ty_Int) → new_sr7(vuz65)
new_sr4(vuz6, bf) → new_sr9(vuz6, vuz6, bf)
new_primPlusNat0(Succ(vuz500), vuz1700) → Succ(Succ(new_primPlusNat1(vuz500, vuz1700)))
new_sr3(vuz65, app(ty_Ratio, be)) → new_sr4(vuz65, be)
new_sr11(Neg(vuz400), Neg(vuz170)) → Pos(new_primMulNat0(vuz400, vuz170))
new_sr(vuz88, vuz89, ty_Integer) → new_sr12(vuz88, vuz89)
new_primPlusNat0(Zero, vuz1700) → Succ(vuz1700)
new_sr0(vuz88, vuz89, ty_Int) → new_sr11(vuz88, vuz89)
new_sr2(vuz65, app(ty_Ratio, be)) → new_sr4(vuz65, be)
new_primDivNatS0(Succ(Succ(vuz5400000))) → Succ(new_primDivNatS0(vuz5400000))
new_sr11(Pos(vuz400), Pos(vuz170)) → Pos(new_primMulNat0(vuz400, vuz170))
new_sr12(vuz38, vuz17) → error([])
new_sr1(vuz53, ty_Integer) → new_sr5(vuz53)
new_primDivNatS0(Succ(Zero)) → Succ(new_primDivNatS1)
new_sr3(vuz65, ty_Double) → new_sr8(vuz65)
new_sr5(vuz6) → new_sr12(vuz6, vuz6)
new_primPlusNat1(Zero, Succ(vuz17000)) → Succ(vuz17000)
new_primPlusNat1(Succ(vuz5000), Zero) → Succ(vuz5000)
new_sr(vuz88, vuz89, ty_Float) → new_sr13(vuz88, vuz89)
new_sr13(Float(vuz390, vuz391), Float(vuz170, vuz171)) → Float(new_sr11(vuz390, vuz170), new_sr11(vuz391, vuz171))
new_primDivNatS0(Zero) → Zero
new_sr3(vuz65, ty_Int) → new_sr7(vuz65)
new_sr1(vuz53, ty_Int) → new_sr7(vuz53)
new_sr7(vuz6) → new_sr11(vuz6, vuz6)

The set Q consists of the following terms:

new_sr2(x0, ty_Float)
new_sr0(x0, x1, ty_Int)
new_sr1(x0, ty_Int)
new_primPlusNat1(Succ(x0), Succ(x1))
new_primMulNat0(Succ(x0), Zero)
new_primMulNat0(Zero, Zero)
new_sr12(x0, x1)
new_sr1(x0, ty_Double)
new_primDivNatS1
new_sr3(x0, app(ty_Ratio, x1))
new_sr3(x0, ty_Float)
new_sr11(Neg(x0), Neg(x1))
new_primPlusNat1(Zero, Zero)
new_sr(x0, x1, ty_Float)
new_sr7(x0)
new_sr0(x0, x1, ty_Integer)
new_sr0(x0, x1, app(ty_Ratio, x2))
new_sr(x0, x1, ty_Int)
new_sr6(x0)
new_sr(x0, x1, ty_Double)
new_sr0(x0, x1, ty_Double)
new_sr9(x0, x1, x2)
new_sr2(x0, ty_Double)
new_sr8(x0)
new_sr(x0, x1, ty_Integer)
new_sr11(Pos(x0), Pos(x1))
new_sr3(x0, ty_Double)
new_primPlusNat1(Succ(x0), Zero)
new_sr3(x0, ty_Int)
new_sr13(Float(x0, x1), Float(x2, x3))
new_sr3(x0, ty_Integer)
new_sr1(x0, app(ty_Ratio, x1))
new_primDivNatS0(Succ(Succ(x0)))
new_sr11(Pos(x0), Neg(x1))
new_sr11(Neg(x0), Pos(x1))
new_sr2(x0, ty_Integer)
new_primDivNatS0(Zero)
new_primDivNatS0(Succ(Zero))
new_primPlusNat0(Succ(x0), x1)
new_sr1(x0, ty_Integer)
new_sr2(x0, app(ty_Ratio, x1))
new_sr4(x0, x1)
new_sr1(x0, ty_Float)
new_sr5(x0)
new_sr(x0, x1, app(ty_Ratio, x2))
new_primPlusNat1(Zero, Succ(x0))
new_primPlusNat0(Zero, x0)
new_primMulNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Succ(x0))
new_sr10(x0, x1)
new_sr0(x0, x1, ty_Float)
new_sr2(x0, ty_Int)

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ AND

                                ↳ QDP

                                  ↳ UsableRulesProof

                                    ↳ QDP

                                      ↳ QReductionProof

                                ↳ QDP

                          ↳ QDP

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_pr2F0G10(vuz52, vuz53, Zero, bc) → new_pr2F0G10(vuz52, new_sr1(vuz53, bc), Zero, bc)

The TRS R consists of the following rules:

new_sr1(vuz53, app(ty_Ratio, bh)) → new_sr4(vuz53, bh)
new_sr1(vuz53, ty_Float) → new_sr6(vuz53)
new_sr1(vuz53, ty_Double) → new_sr8(vuz53)
new_sr1(vuz53, ty_Integer) → new_sr5(vuz53)
new_sr1(vuz53, ty_Int) → new_sr7(vuz53)
new_sr7(vuz6) → new_sr11(vuz6, vuz6)
new_sr11(Neg(vuz400), Neg(vuz170)) → Pos(new_primMulNat0(vuz400, vuz170))
new_sr11(Pos(vuz400), Pos(vuz170)) → Pos(new_primMulNat0(vuz400, vuz170))
new_primMulNat0(Succ(vuz4000), Zero) → Zero
new_primMulNat0(Zero, Succ(vuz1700)) → Zero
new_primMulNat0(Succ(vuz4000), Succ(vuz1700)) → new_primPlusNat0(new_primMulNat0(vuz4000, Succ(vuz1700)), vuz1700)
new_primMulNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(vuz500), vuz1700) → Succ(Succ(new_primPlusNat1(vuz500, vuz1700)))
new_primPlusNat0(Zero, vuz1700) → Succ(vuz1700)
new_primPlusNat1(Succ(vuz5000), Succ(vuz17000)) → Succ(Succ(new_primPlusNat1(vuz5000, vuz17000)))
new_primPlusNat1(Zero, Zero) → Zero
new_primPlusNat1(Zero, Succ(vuz17000)) → Succ(vuz17000)
new_primPlusNat1(Succ(vuz5000), Zero) → Succ(vuz5000)
new_sr5(vuz6) → new_sr12(vuz6, vuz6)
new_sr12(vuz38, vuz17) → error([])
new_sr8(vuz6) → new_sr10(vuz6, vuz6)
new_sr10(vuz41, vuz17) → error([])
new_sr6(vuz6) → new_sr13(vuz6, vuz6)
new_sr13(Float(vuz390, vuz391), Float(vuz170, vuz171)) → Float(new_sr11(vuz390, vuz170), new_sr11(vuz391, vuz171))
new_sr11(Pos(vuz400), Neg(vuz170)) → Neg(new_primMulNat0(vuz400, vuz170))
new_sr11(Neg(vuz400), Pos(vuz170)) → Neg(new_primMulNat0(vuz400, vuz170))
new_sr4(vuz6, bf) → new_sr9(vuz6, vuz6, bf)
new_sr9(vuz13, vuz37, ca) → error([])

The set Q consists of the following terms:

new_sr2(x0, ty_Float)
new_sr0(x0, x1, ty_Int)
new_sr1(x0, ty_Int)
new_primPlusNat1(Succ(x0), Succ(x1))
new_primMulNat0(Succ(x0), Zero)
new_primMulNat0(Zero, Zero)
new_sr12(x0, x1)
new_sr1(x0, ty_Double)
new_primDivNatS1
new_sr3(x0, app(ty_Ratio, x1))
new_sr3(x0, ty_Float)
new_sr11(Neg(x0), Neg(x1))
new_primPlusNat1(Zero, Zero)
new_sr(x0, x1, ty_Float)
new_sr7(x0)
new_sr0(x0, x1, ty_Integer)
new_sr0(x0, x1, app(ty_Ratio, x2))
new_sr(x0, x1, ty_Int)
new_sr6(x0)
new_sr(x0, x1, ty_Double)
new_sr0(x0, x1, ty_Double)
new_sr9(x0, x1, x2)
new_sr2(x0, ty_Double)
new_sr8(x0)
new_sr(x0, x1, ty_Integer)
new_sr11(Pos(x0), Pos(x1))
new_sr3(x0, ty_Double)
new_primPlusNat1(Succ(x0), Zero)
new_sr3(x0, ty_Int)
new_sr13(Float(x0, x1), Float(x2, x3))
new_sr3(x0, ty_Integer)
new_sr1(x0, app(ty_Ratio, x1))
new_primDivNatS0(Succ(Succ(x0)))
new_sr11(Pos(x0), Neg(x1))
new_sr11(Neg(x0), Pos(x1))
new_sr2(x0, ty_Integer)
new_primDivNatS0(Zero)
new_primDivNatS0(Succ(Zero))
new_primPlusNat0(Succ(x0), x1)
new_sr1(x0, ty_Integer)
new_sr2(x0, app(ty_Ratio, x1))
new_sr4(x0, x1)
new_sr1(x0, ty_Float)
new_sr5(x0)
new_sr(x0, x1, app(ty_Ratio, x2))
new_primPlusNat1(Zero, Succ(x0))
new_primPlusNat0(Zero, x0)
new_primMulNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Succ(x0))
new_sr10(x0, x1)
new_sr0(x0, x1, ty_Float)
new_sr2(x0, ty_Int)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_sr2(x0, ty_Float)
new_sr0(x0, x1, ty_Int)
new_primDivNatS1
new_sr3(x0, app(ty_Ratio, x1))
new_sr3(x0, ty_Float)
new_sr(x0, x1, ty_Float)
new_sr0(x0, x1, ty_Integer)
new_sr0(x0, x1, app(ty_Ratio, x2))
new_sr(x0, x1, ty_Int)
new_sr(x0, x1, ty_Double)
new_sr0(x0, x1, ty_Double)
new_sr2(x0, ty_Double)
new_sr(x0, x1, ty_Integer)
new_sr3(x0, ty_Double)
new_sr3(x0, ty_Int)
new_sr3(x0, ty_Integer)
new_primDivNatS0(Succ(Succ(x0)))
new_sr2(x0, ty_Integer)
new_primDivNatS0(Zero)
new_primDivNatS0(Succ(Zero))
new_sr2(x0, app(ty_Ratio, x1))
new_sr(x0, x1, app(ty_Ratio, x2))
new_sr0(x0, x1, ty_Float)
new_sr2(x0, ty_Int)

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ AND

                                ↳ QDP

                                  ↳ UsableRulesProof

                                    ↳ QDP

                                      ↳ QReductionProof

                                        ↳ QDP

                                          ↳ MNOCProof

                                ↳ QDP

                          ↳ QDP

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_pr2F0G10(vuz52, vuz53, Zero, bc) → new_pr2F0G10(vuz52, new_sr1(vuz53, bc), Zero, bc)

The TRS R consists of the following rules:

new_sr1(vuz53, app(ty_Ratio, bh)) → new_sr4(vuz53, bh)
new_sr1(vuz53, ty_Float) → new_sr6(vuz53)
new_sr1(vuz53, ty_Double) → new_sr8(vuz53)
new_sr1(vuz53, ty_Integer) → new_sr5(vuz53)
new_sr1(vuz53, ty_Int) → new_sr7(vuz53)
new_sr7(vuz6) → new_sr11(vuz6, vuz6)
new_sr11(Neg(vuz400), Neg(vuz170)) → Pos(new_primMulNat0(vuz400, vuz170))
new_sr11(Pos(vuz400), Pos(vuz170)) → Pos(new_primMulNat0(vuz400, vuz170))
new_primMulNat0(Succ(vuz4000), Zero) → Zero
new_primMulNat0(Zero, Succ(vuz1700)) → Zero
new_primMulNat0(Succ(vuz4000), Succ(vuz1700)) → new_primPlusNat0(new_primMulNat0(vuz4000, Succ(vuz1700)), vuz1700)
new_primMulNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(vuz500), vuz1700) → Succ(Succ(new_primPlusNat1(vuz500, vuz1700)))
new_primPlusNat0(Zero, vuz1700) → Succ(vuz1700)
new_primPlusNat1(Succ(vuz5000), Succ(vuz17000)) → Succ(Succ(new_primPlusNat1(vuz5000, vuz17000)))
new_primPlusNat1(Zero, Zero) → Zero
new_primPlusNat1(Zero, Succ(vuz17000)) → Succ(vuz17000)
new_primPlusNat1(Succ(vuz5000), Zero) → Succ(vuz5000)
new_sr5(vuz6) → new_sr12(vuz6, vuz6)
new_sr12(vuz38, vuz17) → error([])
new_sr8(vuz6) → new_sr10(vuz6, vuz6)
new_sr10(vuz41, vuz17) → error([])
new_sr6(vuz6) → new_sr13(vuz6, vuz6)
new_sr13(Float(vuz390, vuz391), Float(vuz170, vuz171)) → Float(new_sr11(vuz390, vuz170), new_sr11(vuz391, vuz171))
new_sr11(Pos(vuz400), Neg(vuz170)) → Neg(new_primMulNat0(vuz400, vuz170))
new_sr11(Neg(vuz400), Pos(vuz170)) → Neg(new_primMulNat0(vuz400, vuz170))
new_sr4(vuz6, bf) → new_sr9(vuz6, vuz6, bf)
new_sr9(vuz13, vuz37, ca) → error([])

The set Q consists of the following terms:

new_sr1(x0, ty_Int)
new_primPlusNat1(Succ(x0), Succ(x1))
new_primMulNat0(Succ(x0), Zero)
new_primMulNat0(Zero, Zero)
new_sr12(x0, x1)
new_sr1(x0, ty_Double)
new_sr11(Neg(x0), Neg(x1))
new_primPlusNat1(Zero, Zero)
new_sr7(x0)
new_sr6(x0)
new_sr9(x0, x1, x2)
new_sr8(x0)
new_sr11(Pos(x0), Pos(x1))
new_primPlusNat1(Succ(x0), Zero)
new_sr13(Float(x0, x1), Float(x2, x3))
new_sr1(x0, app(ty_Ratio, x1))
new_sr11(Pos(x0), Neg(x1))
new_sr11(Neg(x0), Pos(x1))
new_primPlusNat0(Succ(x0), x1)
new_sr1(x0, ty_Integer)
new_sr4(x0, x1)
new_sr1(x0, ty_Float)
new_sr5(x0)
new_primPlusNat1(Zero, Succ(x0))
new_primPlusNat0(Zero, x0)
new_primMulNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Succ(x0))
new_sr10(x0, x1)

We have to consider all minimal (P,Q,R)-chains.
We use the modular non-overlap check [17] to decrease Q to the empty set.

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ AND

                                ↳ QDP

                                  ↳ UsableRulesProof

                                    ↳ QDP

                                      ↳ QReductionProof

                                        ↳ QDP

                                          ↳ MNOCProof

                                            ↳ QDP

                                              ↳ NonTerminationProof

                                ↳ QDP

                          ↳ QDP

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_pr2F0G10(vuz52, vuz53, Zero, bc) → new_pr2F0G10(vuz52, new_sr1(vuz53, bc), Zero, bc)

The TRS R consists of the following rules:

new_sr1(vuz53, app(ty_Ratio, bh)) → new_sr4(vuz53, bh)
new_sr1(vuz53, ty_Float) → new_sr6(vuz53)
new_sr1(vuz53, ty_Double) → new_sr8(vuz53)
new_sr1(vuz53, ty_Integer) → new_sr5(vuz53)
new_sr1(vuz53, ty_Int) → new_sr7(vuz53)
new_sr7(vuz6) → new_sr11(vuz6, vuz6)
new_sr11(Neg(vuz400), Neg(vuz170)) → Pos(new_primMulNat0(vuz400, vuz170))
new_sr11(Pos(vuz400), Pos(vuz170)) → Pos(new_primMulNat0(vuz400, vuz170))
new_primMulNat0(Succ(vuz4000), Zero) → Zero
new_primMulNat0(Zero, Succ(vuz1700)) → Zero
new_primMulNat0(Succ(vuz4000), Succ(vuz1700)) → new_primPlusNat0(new_primMulNat0(vuz4000, Succ(vuz1700)), vuz1700)
new_primMulNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(vuz500), vuz1700) → Succ(Succ(new_primPlusNat1(vuz500, vuz1700)))
new_primPlusNat0(Zero, vuz1700) → Succ(vuz1700)
new_primPlusNat1(Succ(vuz5000), Succ(vuz17000)) → Succ(Succ(new_primPlusNat1(vuz5000, vuz17000)))
new_primPlusNat1(Zero, Zero) → Zero
new_primPlusNat1(Zero, Succ(vuz17000)) → Succ(vuz17000)
new_primPlusNat1(Succ(vuz5000), Zero) → Succ(vuz5000)
new_sr5(vuz6) → new_sr12(vuz6, vuz6)
new_sr12(vuz38, vuz17) → error([])
new_sr8(vuz6) → new_sr10(vuz6, vuz6)
new_sr10(vuz41, vuz17) → error([])
new_sr6(vuz6) → new_sr13(vuz6, vuz6)
new_sr13(Float(vuz390, vuz391), Float(vuz170, vuz171)) → Float(new_sr11(vuz390, vuz170), new_sr11(vuz391, vuz171))
new_sr11(Pos(vuz400), Neg(vuz170)) → Neg(new_primMulNat0(vuz400, vuz170))
new_sr11(Neg(vuz400), Pos(vuz170)) → Neg(new_primMulNat0(vuz400, vuz170))
new_sr4(vuz6, bf) → new_sr9(vuz6, vuz6, bf)
new_sr9(vuz13, vuz37, ca) → error([])

Q is empty.
We have to consider all (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

The TRS P consists of the following rules:

new_pr2F0G10(vuz52, vuz53, Zero, bc) → new_pr2F0G10(vuz52, new_sr1(vuz53, bc), Zero, bc)

The TRS R consists of the following rules:

new_sr1(vuz53, app(ty_Ratio, bh)) → new_sr4(vuz53, bh)
new_sr1(vuz53, ty_Float) → new_sr6(vuz53)
new_sr1(vuz53, ty_Double) → new_sr8(vuz53)
new_sr1(vuz53, ty_Integer) → new_sr5(vuz53)
new_sr1(vuz53, ty_Int) → new_sr7(vuz53)
new_sr7(vuz6) → new_sr11(vuz6, vuz6)
new_sr11(Neg(vuz400), Neg(vuz170)) → Pos(new_primMulNat0(vuz400, vuz170))
new_sr11(Pos(vuz400), Pos(vuz170)) → Pos(new_primMulNat0(vuz400, vuz170))
new_primMulNat0(Succ(vuz4000), Zero) → Zero
new_primMulNat0(Zero, Succ(vuz1700)) → Zero
new_primMulNat0(Succ(vuz4000), Succ(vuz1700)) → new_primPlusNat0(new_primMulNat0(vuz4000, Succ(vuz1700)), vuz1700)
new_primMulNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(vuz500), vuz1700) → Succ(Succ(new_primPlusNat1(vuz500, vuz1700)))
new_primPlusNat0(Zero, vuz1700) → Succ(vuz1700)
new_primPlusNat1(Succ(vuz5000), Succ(vuz17000)) → Succ(Succ(new_primPlusNat1(vuz5000, vuz17000)))
new_primPlusNat1(Zero, Zero) → Zero
new_primPlusNat1(Zero, Succ(vuz17000)) → Succ(vuz17000)
new_primPlusNat1(Succ(vuz5000), Zero) → Succ(vuz5000)
new_sr5(vuz6) → new_sr12(vuz6, vuz6)
new_sr12(vuz38, vuz17) → error([])
new_sr8(vuz6) → new_sr10(vuz6, vuz6)
new_sr10(vuz41, vuz17) → error([])
new_sr6(vuz6) → new_sr13(vuz6, vuz6)
new_sr13(Float(vuz390, vuz391), Float(vuz170, vuz171)) → Float(new_sr11(vuz390, vuz170), new_sr11(vuz391, vuz171))
new_sr11(Pos(vuz400), Neg(vuz170)) → Neg(new_primMulNat0(vuz400, vuz170))
new_sr11(Neg(vuz400), Pos(vuz170)) → Neg(new_primMulNat0(vuz400, vuz170))
new_sr4(vuz6, bf) → new_sr9(vuz6, vuz6, bf)
new_sr9(vuz13, vuz37, ca) → error([])

s = new_pr2F0G10(vuz52, vuz53, Zero, bc) evaluates to t =new_pr2F0G10(vuz52, new_sr1(vuz53, bc), Zero, bc)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Matcher: [vuz53 / new_sr1(vuz53, bc)]
Semiunifier: [ ]

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from new_pr2F0G10(vuz52, vuz53, Zero, bc) to new_pr2F0G10(vuz52, new_sr1(vuz53, bc), Zero, bc).

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ AND

                                ↳ QDP

                                ↳ QDP

                                  ↳ UsableRulesProof

                          ↳ QDP

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_pr2F0G1(vuz88, vuz89, vuz90, Succ(Succ(vuz9100)), ba) → new_pr2F0G1(vuz88, vuz89, vuz90, vuz9100, ba)
new_pr2F3(Succ(vuz840), vuz85, vuz86, bb) → new_pr2F0G1(vuz85, vuz86, vuz840, Succ(vuz840), bb)
new_pr2F0G10(vuz52, vuz53, Succ(Succ(Zero)), bc) → new_pr2F0G11(vuz52, vuz53, new_primDivNatS1, Succ(new_primDivNatS1), bc)
new_pr2F0G11(vuz64, vuz65, vuz66, Zero, bd) → new_pr2F0G10(vuz64, new_sr3(vuz65, bd), Succ(vuz66), bd)
new_pr2F0G10(vuz52, vuz53, Succ(Succ(Succ(vuz54000))), bc) → new_pr2F0G11(vuz52, vuz53, new_primDivNatS0(vuz54000), Succ(new_primDivNatS0(vuz54000)), bc)
new_pr2F0G1(vuz88, vuz89, vuz90, Succ(Zero), ba) → new_pr2F3(vuz90, vuz88, new_sr(vuz88, vuz89, ba), ba)
new_pr2F0G1(vuz88, vuz89, vuz90, Zero, ba) → new_pr2F0G10(new_sr0(vuz88, vuz89, ba), vuz88, Succ(vuz90), ba)
new_pr2F0G11(vuz64, vuz65, vuz66, Succ(Succ(vuz6700)), bd) → new_pr2F0G11(vuz64, vuz65, vuz66, vuz6700, bd)
new_pr2F0G11(vuz64, vuz65, vuz66, Succ(Zero), bd) → new_pr2F3(vuz66, new_sr2(vuz65, bd), vuz64, bd)

The TRS R consists of the following rules:

new_sr0(vuz88, vuz89, ty_Integer) → new_sr12(vuz88, vuz89)
new_sr(vuz88, vuz89, ty_Double) → new_sr10(vuz88, vuz89)
new_sr3(vuz65, ty_Float) → new_sr6(vuz65)
new_sr9(vuz13, vuz37, ca) → error([])
new_sr0(vuz88, vuz89, ty_Double) → new_sr10(vuz88, vuz89)
new_primPlusNat1(Succ(vuz5000), Succ(vuz17000)) → Succ(Succ(new_primPlusNat1(vuz5000, vuz17000)))
new_sr3(vuz65, ty_Integer) → new_sr5(vuz65)
new_primMulNat0(Succ(vuz4000), Zero) → Zero
new_primMulNat0(Zero, Succ(vuz1700)) → Zero
new_sr6(vuz6) → new_sr13(vuz6, vuz6)
new_sr1(vuz53, app(ty_Ratio, bh)) → new_sr4(vuz53, bh)
new_sr2(vuz65, ty_Integer) → new_sr5(vuz65)
new_sr2(vuz65, ty_Float) → new_sr6(vuz65)
new_primPlusNat1(Zero, Zero) → Zero
new_sr1(vuz53, ty_Float) → new_sr6(vuz53)
new_sr(vuz88, vuz89, ty_Int) → new_sr11(vuz88, vuz89)
new_sr0(vuz88, vuz89, app(ty_Ratio, bg)) → new_sr9(vuz88, vuz89, bg)
new_primDivNatS1 → Zero
new_primMulNat0(Succ(vuz4000), Succ(vuz1700)) → new_primPlusNat0(new_primMulNat0(vuz4000, Succ(vuz1700)), vuz1700)
new_sr8(vuz6) → new_sr10(vuz6, vuz6)
new_sr0(vuz88, vuz89, ty_Float) → new_sr13(vuz88, vuz89)
new_sr1(vuz53, ty_Double) → new_sr8(vuz53)
new_sr11(Pos(vuz400), Neg(vuz170)) → Neg(new_primMulNat0(vuz400, vuz170))
new_sr11(Neg(vuz400), Pos(vuz170)) → Neg(new_primMulNat0(vuz400, vuz170))
new_sr(vuz88, vuz89, app(ty_Ratio, bg)) → new_sr9(vuz88, vuz89, bg)
new_sr2(vuz65, ty_Double) → new_sr8(vuz65)
new_sr10(vuz41, vuz17) → error([])
new_primMulNat0(Zero, Zero) → Zero
new_sr2(vuz65, ty_Int) → new_sr7(vuz65)
new_sr4(vuz6, bf) → new_sr9(vuz6, vuz6, bf)
new_primPlusNat0(Succ(vuz500), vuz1700) → Succ(Succ(new_primPlusNat1(vuz500, vuz1700)))
new_sr3(vuz65, app(ty_Ratio, be)) → new_sr4(vuz65, be)
new_sr11(Neg(vuz400), Neg(vuz170)) → Pos(new_primMulNat0(vuz400, vuz170))
new_sr(vuz88, vuz89, ty_Integer) → new_sr12(vuz88, vuz89)
new_primPlusNat0(Zero, vuz1700) → Succ(vuz1700)
new_sr0(vuz88, vuz89, ty_Int) → new_sr11(vuz88, vuz89)
new_sr2(vuz65, app(ty_Ratio, be)) → new_sr4(vuz65, be)
new_primDivNatS0(Succ(Succ(vuz5400000))) → Succ(new_primDivNatS0(vuz5400000))
new_sr11(Pos(vuz400), Pos(vuz170)) → Pos(new_primMulNat0(vuz400, vuz170))
new_sr12(vuz38, vuz17) → error([])
new_sr1(vuz53, ty_Integer) → new_sr5(vuz53)
new_primDivNatS0(Succ(Zero)) → Succ(new_primDivNatS1)
new_sr3(vuz65, ty_Double) → new_sr8(vuz65)
new_sr5(vuz6) → new_sr12(vuz6, vuz6)
new_primPlusNat1(Zero, Succ(vuz17000)) → Succ(vuz17000)
new_primPlusNat1(Succ(vuz5000), Zero) → Succ(vuz5000)
new_sr(vuz88, vuz89, ty_Float) → new_sr13(vuz88, vuz89)
new_sr13(Float(vuz390, vuz391), Float(vuz170, vuz171)) → Float(new_sr11(vuz390, vuz170), new_sr11(vuz391, vuz171))
new_primDivNatS0(Zero) → Zero
new_sr3(vuz65, ty_Int) → new_sr7(vuz65)
new_sr1(vuz53, ty_Int) → new_sr7(vuz53)
new_sr7(vuz6) → new_sr11(vuz6, vuz6)

The set Q consists of the following terms:

new_sr2(x0, ty_Float)
new_sr0(x0, x1, ty_Int)
new_sr1(x0, ty_Int)
new_primPlusNat1(Succ(x0), Succ(x1))
new_primMulNat0(Succ(x0), Zero)
new_primMulNat0(Zero, Zero)
new_sr12(x0, x1)
new_sr1(x0, ty_Double)
new_primDivNatS1
new_sr3(x0, app(ty_Ratio, x1))
new_sr3(x0, ty_Float)
new_sr11(Neg(x0), Neg(x1))
new_primPlusNat1(Zero, Zero)
new_sr(x0, x1, ty_Float)
new_sr7(x0)
new_sr0(x0, x1, ty_Integer)
new_sr0(x0, x1, app(ty_Ratio, x2))
new_sr(x0, x1, ty_Int)
new_sr6(x0)
new_sr(x0, x1, ty_Double)
new_sr0(x0, x1, ty_Double)
new_sr9(x0, x1, x2)
new_sr2(x0, ty_Double)
new_sr8(x0)
new_sr(x0, x1, ty_Integer)
new_sr11(Pos(x0), Pos(x1))
new_sr3(x0, ty_Double)
new_primPlusNat1(Succ(x0), Zero)
new_sr3(x0, ty_Int)
new_sr13(Float(x0, x1), Float(x2, x3))
new_sr3(x0, ty_Integer)
new_sr1(x0, app(ty_Ratio, x1))
new_primDivNatS0(Succ(Succ(x0)))
new_sr11(Pos(x0), Neg(x1))
new_sr11(Neg(x0), Pos(x1))
new_sr2(x0, ty_Integer)
new_primDivNatS0(Zero)
new_primDivNatS0(Succ(Zero))
new_primPlusNat0(Succ(x0), x1)
new_sr1(x0, ty_Integer)
new_sr2(x0, app(ty_Ratio, x1))
new_sr4(x0, x1)
new_sr1(x0, ty_Float)
new_sr5(x0)
new_sr(x0, x1, app(ty_Ratio, x2))
new_primPlusNat1(Zero, Succ(x0))
new_primPlusNat0(Zero, x0)
new_primMulNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Succ(x0))
new_sr10(x0, x1)
new_sr0(x0, x1, ty_Float)
new_sr2(x0, ty_Int)

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ AND

                                ↳ QDP

                                ↳ QDP

                                  ↳ UsableRulesProof

                                    ↳ QDP

                                      ↳ QReductionProof

                          ↳ QDP

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_pr2F0G1(vuz88, vuz89, vuz90, Succ(Succ(vuz9100)), ba) → new_pr2F0G1(vuz88, vuz89, vuz90, vuz9100, ba)
new_pr2F3(Succ(vuz840), vuz85, vuz86, bb) → new_pr2F0G1(vuz85, vuz86, vuz840, Succ(vuz840), bb)
new_pr2F0G10(vuz52, vuz53, Succ(Succ(Zero)), bc) → new_pr2F0G11(vuz52, vuz53, new_primDivNatS1, Succ(new_primDivNatS1), bc)
new_pr2F0G11(vuz64, vuz65, vuz66, Zero, bd) → new_pr2F0G10(vuz64, new_sr3(vuz65, bd), Succ(vuz66), bd)
new_pr2F0G10(vuz52, vuz53, Succ(Succ(Succ(vuz54000))), bc) → new_pr2F0G11(vuz52, vuz53, new_primDivNatS0(vuz54000), Succ(new_primDivNatS0(vuz54000)), bc)
new_pr2F0G1(vuz88, vuz89, vuz90, Succ(Zero), ba) → new_pr2F3(vuz90, vuz88, new_sr(vuz88, vuz89, ba), ba)
new_pr2F0G1(vuz88, vuz89, vuz90, Zero, ba) → new_pr2F0G10(new_sr0(vuz88, vuz89, ba), vuz88, Succ(vuz90), ba)
new_pr2F0G11(vuz64, vuz65, vuz66, Succ(Succ(vuz6700)), bd) → new_pr2F0G11(vuz64, vuz65, vuz66, vuz6700, bd)
new_pr2F0G11(vuz64, vuz65, vuz66, Succ(Zero), bd) → new_pr2F3(vuz66, new_sr2(vuz65, bd), vuz64, bd)

The TRS R consists of the following rules:

new_sr0(vuz88, vuz89, ty_Integer) → new_sr12(vuz88, vuz89)
new_sr0(vuz88, vuz89, ty_Double) → new_sr10(vuz88, vuz89)
new_sr0(vuz88, vuz89, app(ty_Ratio, bg)) → new_sr9(vuz88, vuz89, bg)
new_sr0(vuz88, vuz89, ty_Float) → new_sr13(vuz88, vuz89)
new_sr0(vuz88, vuz89, ty_Int) → new_sr11(vuz88, vuz89)
new_sr11(Pos(vuz400), Neg(vuz170)) → Neg(new_primMulNat0(vuz400, vuz170))
new_sr11(Neg(vuz400), Pos(vuz170)) → Neg(new_primMulNat0(vuz400, vuz170))
new_sr11(Neg(vuz400), Neg(vuz170)) → Pos(new_primMulNat0(vuz400, vuz170))
new_sr11(Pos(vuz400), Pos(vuz170)) → Pos(new_primMulNat0(vuz400, vuz170))
new_primMulNat0(Succ(vuz4000), Zero) → Zero
new_primMulNat0(Zero, Succ(vuz1700)) → Zero
new_primMulNat0(Succ(vuz4000), Succ(vuz1700)) → new_primPlusNat0(new_primMulNat0(vuz4000, Succ(vuz1700)), vuz1700)
new_primMulNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(vuz500), vuz1700) → Succ(Succ(new_primPlusNat1(vuz500, vuz1700)))
new_primPlusNat0(Zero, vuz1700) → Succ(vuz1700)
new_primPlusNat1(Succ(vuz5000), Succ(vuz17000)) → Succ(Succ(new_primPlusNat1(vuz5000, vuz17000)))
new_primPlusNat1(Zero, Zero) → Zero
new_primPlusNat1(Zero, Succ(vuz17000)) → Succ(vuz17000)
new_primPlusNat1(Succ(vuz5000), Zero) → Succ(vuz5000)
new_sr13(Float(vuz390, vuz391), Float(vuz170, vuz171)) → Float(new_sr11(vuz390, vuz170), new_sr11(vuz391, vuz171))
new_sr9(vuz13, vuz37, ca) → error([])
new_sr10(vuz41, vuz17) → error([])
new_sr12(vuz38, vuz17) → error([])
new_primDivNatS0(Succ(Succ(vuz5400000))) → Succ(new_primDivNatS0(vuz5400000))
new_primDivNatS0(Succ(Zero)) → Succ(new_primDivNatS1)
new_primDivNatS0(Zero) → Zero
new_primDivNatS1 → Zero
new_sr3(vuz65, ty_Float) → new_sr6(vuz65)
new_sr3(vuz65, ty_Integer) → new_sr5(vuz65)
new_sr3(vuz65, app(ty_Ratio, be)) → new_sr4(vuz65, be)
new_sr3(vuz65, ty_Double) → new_sr8(vuz65)
new_sr3(vuz65, ty_Int) → new_sr7(vuz65)
new_sr7(vuz6) → new_sr11(vuz6, vuz6)
new_sr8(vuz6) → new_sr10(vuz6, vuz6)
new_sr4(vuz6, bf) → new_sr9(vuz6, vuz6, bf)
new_sr5(vuz6) → new_sr12(vuz6, vuz6)
new_sr6(vuz6) → new_sr13(vuz6, vuz6)
new_sr2(vuz65, ty_Integer) → new_sr5(vuz65)
new_sr2(vuz65, ty_Float) → new_sr6(vuz65)
new_sr2(vuz65, ty_Double) → new_sr8(vuz65)
new_sr2(vuz65, ty_Int) → new_sr7(vuz65)
new_sr2(vuz65, app(ty_Ratio, be)) → new_sr4(vuz65, be)
new_sr(vuz88, vuz89, ty_Double) → new_sr10(vuz88, vuz89)
new_sr(vuz88, vuz89, ty_Int) → new_sr11(vuz88, vuz89)
new_sr(vuz88, vuz89, app(ty_Ratio, bg)) → new_sr9(vuz88, vuz89, bg)
new_sr(vuz88, vuz89, ty_Integer) → new_sr12(vuz88, vuz89)
new_sr(vuz88, vuz89, ty_Float) → new_sr13(vuz88, vuz89)

The set Q consists of the following terms:

new_sr2(x0, ty_Float)
new_sr0(x0, x1, ty_Int)
new_sr1(x0, ty_Int)
new_primPlusNat1(Succ(x0), Succ(x1))
new_primMulNat0(Succ(x0), Zero)
new_primMulNat0(Zero, Zero)
new_sr12(x0, x1)
new_sr1(x0, ty_Double)
new_primDivNatS1
new_sr3(x0, app(ty_Ratio, x1))
new_sr3(x0, ty_Float)
new_sr11(Neg(x0), Neg(x1))
new_primPlusNat1(Zero, Zero)
new_sr(x0, x1, ty_Float)
new_sr7(x0)
new_sr0(x0, x1, ty_Integer)
new_sr0(x0, x1, app(ty_Ratio, x2))
new_sr(x0, x1, ty_Int)
new_sr6(x0)
new_sr(x0, x1, ty_Double)
new_sr0(x0, x1, ty_Double)
new_sr9(x0, x1, x2)
new_sr2(x0, ty_Double)
new_sr8(x0)
new_sr(x0, x1, ty_Integer)
new_sr11(Pos(x0), Pos(x1))
new_sr3(x0, ty_Double)
new_primPlusNat1(Succ(x0), Zero)
new_sr3(x0, ty_Int)
new_sr13(Float(x0, x1), Float(x2, x3))
new_sr3(x0, ty_Integer)
new_sr1(x0, app(ty_Ratio, x1))
new_primDivNatS0(Succ(Succ(x0)))
new_sr11(Pos(x0), Neg(x1))
new_sr11(Neg(x0), Pos(x1))
new_sr2(x0, ty_Integer)
new_primDivNatS0(Zero)
new_primDivNatS0(Succ(Zero))
new_primPlusNat0(Succ(x0), x1)
new_sr1(x0, ty_Integer)
new_sr2(x0, app(ty_Ratio, x1))
new_sr4(x0, x1)
new_sr1(x0, ty_Float)
new_sr5(x0)
new_sr(x0, x1, app(ty_Ratio, x2))
new_primPlusNat1(Zero, Succ(x0))
new_primPlusNat0(Zero, x0)
new_primMulNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Succ(x0))
new_sr10(x0, x1)
new_sr0(x0, x1, ty_Float)
new_sr2(x0, ty_Int)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_sr1(x0, ty_Int)
new_sr1(x0, ty_Double)
new_sr1(x0, app(ty_Ratio, x1))
new_sr1(x0, ty_Integer)
new_sr1(x0, ty_Float)

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ AND

                                ↳ QDP

                                ↳ QDP

                                  ↳ UsableRulesProof

                                    ↳ QDP

                                      ↳ QReductionProof

                                        ↳ QDP

                                          ↳ Rewriting

                          ↳ QDP

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_pr2F0G1(vuz88, vuz89, vuz90, Succ(Succ(vuz9100)), ba) → new_pr2F0G1(vuz88, vuz89, vuz90, vuz9100, ba)
new_pr2F3(Succ(vuz840), vuz85, vuz86, bb) → new_pr2F0G1(vuz85, vuz86, vuz840, Succ(vuz840), bb)
new_pr2F0G10(vuz52, vuz53, Succ(Succ(Zero)), bc) → new_pr2F0G11(vuz52, vuz53, new_primDivNatS1, Succ(new_primDivNatS1), bc)
new_pr2F0G1(vuz88, vuz89, vuz90, Succ(Zero), ba) → new_pr2F3(vuz90, vuz88, new_sr(vuz88, vuz89, ba), ba)
new_pr2F0G10(vuz52, vuz53, Succ(Succ(Succ(vuz54000))), bc) → new_pr2F0G11(vuz52, vuz53, new_primDivNatS0(vuz54000), Succ(new_primDivNatS0(vuz54000)), bc)
new_pr2F0G11(vuz64, vuz65, vuz66, Zero, bd) → new_pr2F0G10(vuz64, new_sr3(vuz65, bd), Succ(vuz66), bd)
new_pr2F0G1(vuz88, vuz89, vuz90, Zero, ba) → new_pr2F0G10(new_sr0(vuz88, vuz89, ba), vuz88, Succ(vuz90), ba)
new_pr2F0G11(vuz64, vuz65, vuz66, Succ(Succ(vuz6700)), bd) → new_pr2F0G11(vuz64, vuz65, vuz66, vuz6700, bd)
new_pr2F0G11(vuz64, vuz65, vuz66, Succ(Zero), bd) → new_pr2F3(vuz66, new_sr2(vuz65, bd), vuz64, bd)

The TRS R consists of the following rules:

new_sr0(vuz88, vuz89, ty_Integer) → new_sr12(vuz88, vuz89)
new_sr0(vuz88, vuz89, ty_Double) → new_sr10(vuz88, vuz89)
new_sr0(vuz88, vuz89, app(ty_Ratio, bg)) → new_sr9(vuz88, vuz89, bg)
new_sr0(vuz88, vuz89, ty_Float) → new_sr13(vuz88, vuz89)
new_sr0(vuz88, vuz89, ty_Int) → new_sr11(vuz88, vuz89)
new_sr11(Pos(vuz400), Neg(vuz170)) → Neg(new_primMulNat0(vuz400, vuz170))
new_sr11(Neg(vuz400), Pos(vuz170)) → Neg(new_primMulNat0(vuz400, vuz170))
new_sr11(Neg(vuz400), Neg(vuz170)) → Pos(new_primMulNat0(vuz400, vuz170))
new_sr11(Pos(vuz400), Pos(vuz170)) → Pos(new_primMulNat0(vuz400, vuz170))
new_primMulNat0(Succ(vuz4000), Zero) → Zero
new_primMulNat0(Zero, Succ(vuz1700)) → Zero
new_primMulNat0(Succ(vuz4000), Succ(vuz1700)) → new_primPlusNat0(new_primMulNat0(vuz4000, Succ(vuz1700)), vuz1700)
new_primMulNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(vuz500), vuz1700) → Succ(Succ(new_primPlusNat1(vuz500, vuz1700)))
new_primPlusNat0(Zero, vuz1700) → Succ(vuz1700)
new_primPlusNat1(Succ(vuz5000), Succ(vuz17000)) → Succ(Succ(new_primPlusNat1(vuz5000, vuz17000)))
new_primPlusNat1(Zero, Zero) → Zero
new_primPlusNat1(Zero, Succ(vuz17000)) → Succ(vuz17000)
new_primPlusNat1(Succ(vuz5000), Zero) → Succ(vuz5000)
new_sr13(Float(vuz390, vuz391), Float(vuz170, vuz171)) → Float(new_sr11(vuz390, vuz170), new_sr11(vuz391, vuz171))
new_sr9(vuz13, vuz37, ca) → error([])
new_sr10(vuz41, vuz17) → error([])
new_sr12(vuz38, vuz17) → error([])
new_primDivNatS0(Succ(Succ(vuz5400000))) → Succ(new_primDivNatS0(vuz5400000))
new_primDivNatS0(Succ(Zero)) → Succ(new_primDivNatS1)
new_primDivNatS0(Zero) → Zero
new_primDivNatS1 → Zero
new_sr3(vuz65, ty_Float) → new_sr6(vuz65)
new_sr3(vuz65, ty_Integer) → new_sr5(vuz65)
new_sr3(vuz65, app(ty_Ratio, be)) → new_sr4(vuz65, be)
new_sr3(vuz65, ty_Double) → new_sr8(vuz65)
new_sr3(vuz65, ty_Int) → new_sr7(vuz65)
new_sr7(vuz6) → new_sr11(vuz6, vuz6)
new_sr8(vuz6) → new_sr10(vuz6, vuz6)
new_sr4(vuz6, bf) → new_sr9(vuz6, vuz6, bf)
new_sr5(vuz6) → new_sr12(vuz6, vuz6)
new_sr6(vuz6) → new_sr13(vuz6, vuz6)
new_sr2(vuz65, ty_Integer) → new_sr5(vuz65)
new_sr2(vuz65, ty_Float) → new_sr6(vuz65)
new_sr2(vuz65, ty_Double) → new_sr8(vuz65)
new_sr2(vuz65, ty_Int) → new_sr7(vuz65)
new_sr2(vuz65, app(ty_Ratio, be)) → new_sr4(vuz65, be)
new_sr(vuz88, vuz89, ty_Double) → new_sr10(vuz88, vuz89)
new_sr(vuz88, vuz89, ty_Int) → new_sr11(vuz88, vuz89)
new_sr(vuz88, vuz89, app(ty_Ratio, bg)) → new_sr9(vuz88, vuz89, bg)
new_sr(vuz88, vuz89, ty_Integer) → new_sr12(vuz88, vuz89)
new_sr(vuz88, vuz89, ty_Float) → new_sr13(vuz88, vuz89)

The set Q consists of the following terms:

new_sr2(x0, ty_Float)
new_sr0(x0, x1, ty_Int)
new_primPlusNat1(Succ(x0), Succ(x1))
new_primMulNat0(Succ(x0), Zero)
new_primMulNat0(Zero, Zero)
new_sr12(x0, x1)
new_primDivNatS1
new_sr3(x0, app(ty_Ratio, x1))
new_sr3(x0, ty_Float)
new_sr11(Neg(x0), Neg(x1))
new_primPlusNat1(Zero, Zero)
new_sr(x0, x1, ty_Float)
new_sr7(x0)
new_sr0(x0, x1, ty_Integer)
new_sr0(x0, x1, app(ty_Ratio, x2))
new_sr(x0, x1, ty_Int)
new_sr6(x0)
new_sr(x0, x1, ty_Double)
new_sr0(x0, x1, ty_Double)
new_sr9(x0, x1, x2)
new_sr2(x0, ty_Double)
new_sr8(x0)
new_sr(x0, x1, ty_Integer)
new_sr11(Pos(x0), Pos(x1))
new_sr3(x0, ty_Double)
new_primPlusNat1(Succ(x0), Zero)
new_sr3(x0, ty_Int)
new_sr13(Float(x0, x1), Float(x2, x3))
new_sr3(x0, ty_Integer)
new_primDivNatS0(Succ(Succ(x0)))
new_sr11(Pos(x0), Neg(x1))
new_sr11(Neg(x0), Pos(x1))
new_sr2(x0, ty_Integer)
new_primDivNatS0(Zero)
new_primDivNatS0(Succ(Zero))
new_primPlusNat0(Succ(x0), x1)
new_sr2(x0, app(ty_Ratio, x1))
new_sr4(x0, x1)
new_sr5(x0)
new_sr(x0, x1, app(ty_Ratio, x2))
new_primPlusNat1(Zero, Succ(x0))
new_primPlusNat0(Zero, x0)
new_primMulNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Succ(x0))
new_sr10(x0, x1)
new_sr0(x0, x1, ty_Float)
new_sr2(x0, ty_Int)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule new_pr2F0G10(vuz52, vuz53, Succ(Succ(Zero)), bc) → new_pr2F0G11(vuz52, vuz53, new_primDivNatS1, Succ(new_primDivNatS1), bc) at position [2] we obtained the following new rules:

new_pr2F0G10(vuz52, vuz53, Succ(Succ(Zero)), bc) → new_pr2F0G11(vuz52, vuz53, Zero, Succ(new_primDivNatS1), bc)

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ AND

                                ↳ QDP

                                ↳ QDP

                                  ↳ UsableRulesProof

                                    ↳ QDP

                                      ↳ QReductionProof

                                        ↳ QDP

                                          ↳ Rewriting

                                            ↳ QDP

                                              ↳ Rewriting

                          ↳ QDP

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_pr2F0G1(vuz88, vuz89, vuz90, Succ(Succ(vuz9100)), ba) → new_pr2F0G1(vuz88, vuz89, vuz90, vuz9100, ba)
new_pr2F3(Succ(vuz840), vuz85, vuz86, bb) → new_pr2F0G1(vuz85, vuz86, vuz840, Succ(vuz840), bb)
new_pr2F0G10(vuz52, vuz53, Succ(Succ(Zero)), bc) → new_pr2F0G11(vuz52, vuz53, Zero, Succ(new_primDivNatS1), bc)
new_pr2F0G11(vuz64, vuz65, vuz66, Zero, bd) → new_pr2F0G10(vuz64, new_sr3(vuz65, bd), Succ(vuz66), bd)
new_pr2F0G10(vuz52, vuz53, Succ(Succ(Succ(vuz54000))), bc) → new_pr2F0G11(vuz52, vuz53, new_primDivNatS0(vuz54000), Succ(new_primDivNatS0(vuz54000)), bc)
new_pr2F0G1(vuz88, vuz89, vuz90, Succ(Zero), ba) → new_pr2F3(vuz90, vuz88, new_sr(vuz88, vuz89, ba), ba)
new_pr2F0G1(vuz88, vuz89, vuz90, Zero, ba) → new_pr2F0G10(new_sr0(vuz88, vuz89, ba), vuz88, Succ(vuz90), ba)
new_pr2F0G11(vuz64, vuz65, vuz66, Succ(Succ(vuz6700)), bd) → new_pr2F0G11(vuz64, vuz65, vuz66, vuz6700, bd)
new_pr2F0G11(vuz64, vuz65, vuz66, Succ(Zero), bd) → new_pr2F3(vuz66, new_sr2(vuz65, bd), vuz64, bd)

The TRS R consists of the following rules:

new_sr0(vuz88, vuz89, ty_Integer) → new_sr12(vuz88, vuz89)
new_sr0(vuz88, vuz89, ty_Double) → new_sr10(vuz88, vuz89)
new_sr0(vuz88, vuz89, app(ty_Ratio, bg)) → new_sr9(vuz88, vuz89, bg)
new_sr0(vuz88, vuz89, ty_Float) → new_sr13(vuz88, vuz89)
new_sr0(vuz88, vuz89, ty_Int) → new_sr11(vuz88, vuz89)
new_sr11(Pos(vuz400), Neg(vuz170)) → Neg(new_primMulNat0(vuz400, vuz170))
new_sr11(Neg(vuz400), Pos(vuz170)) → Neg(new_primMulNat0(vuz400, vuz170))
new_sr11(Neg(vuz400), Neg(vuz170)) → Pos(new_primMulNat0(vuz400, vuz170))
new_sr11(Pos(vuz400), Pos(vuz170)) → Pos(new_primMulNat0(vuz400, vuz170))
new_primMulNat0(Succ(vuz4000), Zero) → Zero
new_primMulNat0(Zero, Succ(vuz1700)) → Zero
new_primMulNat0(Succ(vuz4000), Succ(vuz1700)) → new_primPlusNat0(new_primMulNat0(vuz4000, Succ(vuz1700)), vuz1700)
new_primMulNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(vuz500), vuz1700) → Succ(Succ(new_primPlusNat1(vuz500, vuz1700)))
new_primPlusNat0(Zero, vuz1700) → Succ(vuz1700)
new_primPlusNat1(Succ(vuz5000), Succ(vuz17000)) → Succ(Succ(new_primPlusNat1(vuz5000, vuz17000)))
new_primPlusNat1(Zero, Zero) → Zero
new_primPlusNat1(Zero, Succ(vuz17000)) → Succ(vuz17000)
new_primPlusNat1(Succ(vuz5000), Zero) → Succ(vuz5000)
new_sr13(Float(vuz390, vuz391), Float(vuz170, vuz171)) → Float(new_sr11(vuz390, vuz170), new_sr11(vuz391, vuz171))
new_sr9(vuz13, vuz37, ca) → error([])
new_sr10(vuz41, vuz17) → error([])
new_sr12(vuz38, vuz17) → error([])
new_primDivNatS0(Succ(Succ(vuz5400000))) → Succ(new_primDivNatS0(vuz5400000))
new_primDivNatS0(Succ(Zero)) → Succ(new_primDivNatS1)
new_primDivNatS0(Zero) → Zero
new_primDivNatS1 → Zero
new_sr3(vuz65, ty_Float) → new_sr6(vuz65)
new_sr3(vuz65, ty_Integer) → new_sr5(vuz65)
new_sr3(vuz65, app(ty_Ratio, be)) → new_sr4(vuz65, be)
new_sr3(vuz65, ty_Double) → new_sr8(vuz65)
new_sr3(vuz65, ty_Int) → new_sr7(vuz65)
new_sr7(vuz6) → new_sr11(vuz6, vuz6)
new_sr8(vuz6) → new_sr10(vuz6, vuz6)
new_sr4(vuz6, bf) → new_sr9(vuz6, vuz6, bf)
new_sr5(vuz6) → new_sr12(vuz6, vuz6)
new_sr6(vuz6) → new_sr13(vuz6, vuz6)
new_sr2(vuz65, ty_Integer) → new_sr5(vuz65)
new_sr2(vuz65, ty_Float) → new_sr6(vuz65)
new_sr2(vuz65, ty_Double) → new_sr8(vuz65)
new_sr2(vuz65, ty_Int) → new_sr7(vuz65)
new_sr2(vuz65, app(ty_Ratio, be)) → new_sr4(vuz65, be)
new_sr(vuz88, vuz89, ty_Double) → new_sr10(vuz88, vuz89)
new_sr(vuz88, vuz89, ty_Int) → new_sr11(vuz88, vuz89)
new_sr(vuz88, vuz89, app(ty_Ratio, bg)) → new_sr9(vuz88, vuz89, bg)
new_sr(vuz88, vuz89, ty_Integer) → new_sr12(vuz88, vuz89)
new_sr(vuz88, vuz89, ty_Float) → new_sr13(vuz88, vuz89)

The set Q consists of the following terms:

new_sr2(x0, ty_Float)
new_sr0(x0, x1, ty_Int)
new_primPlusNat1(Succ(x0), Succ(x1))
new_primMulNat0(Succ(x0), Zero)
new_primMulNat0(Zero, Zero)
new_sr12(x0, x1)
new_primDivNatS1
new_sr3(x0, app(ty_Ratio, x1))
new_sr3(x0, ty_Float)
new_sr11(Neg(x0), Neg(x1))
new_primPlusNat1(Zero, Zero)
new_sr(x0, x1, ty_Float)
new_sr7(x0)
new_sr0(x0, x1, ty_Integer)
new_sr0(x0, x1, app(ty_Ratio, x2))
new_sr(x0, x1, ty_Int)
new_sr6(x0)
new_sr(x0, x1, ty_Double)
new_sr0(x0, x1, ty_Double)
new_sr9(x0, x1, x2)
new_sr2(x0, ty_Double)
new_sr8(x0)
new_sr(x0, x1, ty_Integer)
new_sr11(Pos(x0), Pos(x1))
new_sr3(x0, ty_Double)
new_primPlusNat1(Succ(x0), Zero)
new_sr3(x0, ty_Int)
new_sr13(Float(x0, x1), Float(x2, x3))
new_sr3(x0, ty_Integer)
new_primDivNatS0(Succ(Succ(x0)))
new_sr11(Pos(x0), Neg(x1))
new_sr11(Neg(x0), Pos(x1))
new_sr2(x0, ty_Integer)
new_primDivNatS0(Zero)
new_primDivNatS0(Succ(Zero))
new_primPlusNat0(Succ(x0), x1)
new_sr2(x0, app(ty_Ratio, x1))
new_sr4(x0, x1)
new_sr5(x0)
new_sr(x0, x1, app(ty_Ratio, x2))
new_primPlusNat1(Zero, Succ(x0))
new_primPlusNat0(Zero, x0)
new_primMulNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Succ(x0))
new_sr10(x0, x1)
new_sr0(x0, x1, ty_Float)
new_sr2(x0, ty_Int)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule new_pr2F0G10(vuz52, vuz53, Succ(Succ(Zero)), bc) → new_pr2F0G11(vuz52, vuz53, Zero, Succ(new_primDivNatS1), bc) at position [3,0] we obtained the following new rules:

new_pr2F0G10(vuz52, vuz53, Succ(Succ(Zero)), bc) → new_pr2F0G11(vuz52, vuz53, Zero, Succ(Zero), bc)

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ AND

                                ↳ QDP

                                ↳ QDP

                                  ↳ UsableRulesProof

                                    ↳ QDP

                                      ↳ QReductionProof

                                        ↳ QDP

                                          ↳ Rewriting

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ QDPOrderProof

                          ↳ QDP

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_pr2F0G1(vuz88, vuz89, vuz90, Succ(Succ(vuz9100)), ba) → new_pr2F0G1(vuz88, vuz89, vuz90, vuz9100, ba)
new_pr2F3(Succ(vuz840), vuz85, vuz86, bb) → new_pr2F0G1(vuz85, vuz86, vuz840, Succ(vuz840), bb)
new_pr2F0G10(vuz52, vuz53, Succ(Succ(Zero)), bc) → new_pr2F0G11(vuz52, vuz53, Zero, Succ(Zero), bc)
new_pr2F0G1(vuz88, vuz89, vuz90, Succ(Zero), ba) → new_pr2F3(vuz90, vuz88, new_sr(vuz88, vuz89, ba), ba)
new_pr2F0G10(vuz52, vuz53, Succ(Succ(Succ(vuz54000))), bc) → new_pr2F0G11(vuz52, vuz53, new_primDivNatS0(vuz54000), Succ(new_primDivNatS0(vuz54000)), bc)
new_pr2F0G11(vuz64, vuz65, vuz66, Zero, bd) → new_pr2F0G10(vuz64, new_sr3(vuz65, bd), Succ(vuz66), bd)
new_pr2F0G1(vuz88, vuz89, vuz90, Zero, ba) → new_pr2F0G10(new_sr0(vuz88, vuz89, ba), vuz88, Succ(vuz90), ba)
new_pr2F0G11(vuz64, vuz65, vuz66, Succ(Succ(vuz6700)), bd) → new_pr2F0G11(vuz64, vuz65, vuz66, vuz6700, bd)
new_pr2F0G11(vuz64, vuz65, vuz66, Succ(Zero), bd) → new_pr2F3(vuz66, new_sr2(vuz65, bd), vuz64, bd)

The TRS R consists of the following rules:

new_sr0(vuz88, vuz89, ty_Integer) → new_sr12(vuz88, vuz89)
new_sr0(vuz88, vuz89, ty_Double) → new_sr10(vuz88, vuz89)
new_sr0(vuz88, vuz89, app(ty_Ratio, bg)) → new_sr9(vuz88, vuz89, bg)
new_sr0(vuz88, vuz89, ty_Float) → new_sr13(vuz88, vuz89)
new_sr0(vuz88, vuz89, ty_Int) → new_sr11(vuz88, vuz89)
new_sr11(Pos(vuz400), Neg(vuz170)) → Neg(new_primMulNat0(vuz400, vuz170))
new_sr11(Neg(vuz400), Pos(vuz170)) → Neg(new_primMulNat0(vuz400, vuz170))
new_sr11(Neg(vuz400), Neg(vuz170)) → Pos(new_primMulNat0(vuz400, vuz170))
new_sr11(Pos(vuz400), Pos(vuz170)) → Pos(new_primMulNat0(vuz400, vuz170))
new_primMulNat0(Succ(vuz4000), Zero) → Zero
new_primMulNat0(Zero, Succ(vuz1700)) → Zero
new_primMulNat0(Succ(vuz4000), Succ(vuz1700)) → new_primPlusNat0(new_primMulNat0(vuz4000, Succ(vuz1700)), vuz1700)
new_primMulNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(vuz500), vuz1700) → Succ(Succ(new_primPlusNat1(vuz500, vuz1700)))
new_primPlusNat0(Zero, vuz1700) → Succ(vuz1700)
new_primPlusNat1(Succ(vuz5000), Succ(vuz17000)) → Succ(Succ(new_primPlusNat1(vuz5000, vuz17000)))
new_primPlusNat1(Zero, Zero) → Zero
new_primPlusNat1(Zero, Succ(vuz17000)) → Succ(vuz17000)
new_primPlusNat1(Succ(vuz5000), Zero) → Succ(vuz5000)
new_sr13(Float(vuz390, vuz391), Float(vuz170, vuz171)) → Float(new_sr11(vuz390, vuz170), new_sr11(vuz391, vuz171))
new_sr9(vuz13, vuz37, ca) → error([])
new_sr10(vuz41, vuz17) → error([])
new_sr12(vuz38, vuz17) → error([])
new_primDivNatS0(Succ(Succ(vuz5400000))) → Succ(new_primDivNatS0(vuz5400000))
new_primDivNatS0(Succ(Zero)) → Succ(new_primDivNatS1)
new_primDivNatS0(Zero) → Zero
new_primDivNatS1 → Zero
new_sr3(vuz65, ty_Float) → new_sr6(vuz65)
new_sr3(vuz65, ty_Integer) → new_sr5(vuz65)
new_sr3(vuz65, app(ty_Ratio, be)) → new_sr4(vuz65, be)
new_sr3(vuz65, ty_Double) → new_sr8(vuz65)
new_sr3(vuz65, ty_Int) → new_sr7(vuz65)
new_sr7(vuz6) → new_sr11(vuz6, vuz6)
new_sr8(vuz6) → new_sr10(vuz6, vuz6)
new_sr4(vuz6, bf) → new_sr9(vuz6, vuz6, bf)
new_sr5(vuz6) → new_sr12(vuz6, vuz6)
new_sr6(vuz6) → new_sr13(vuz6, vuz6)
new_sr2(vuz65, ty_Integer) → new_sr5(vuz65)
new_sr2(vuz65, ty_Float) → new_sr6(vuz65)
new_sr2(vuz65, ty_Double) → new_sr8(vuz65)
new_sr2(vuz65, ty_Int) → new_sr7(vuz65)
new_sr2(vuz65, app(ty_Ratio, be)) → new_sr4(vuz65, be)
new_sr(vuz88, vuz89, ty_Double) → new_sr10(vuz88, vuz89)
new_sr(vuz88, vuz89, ty_Int) → new_sr11(vuz88, vuz89)
new_sr(vuz88, vuz89, app(ty_Ratio, bg)) → new_sr9(vuz88, vuz89, bg)
new_sr(vuz88, vuz89, ty_Integer) → new_sr12(vuz88, vuz89)
new_sr(vuz88, vuz89, ty_Float) → new_sr13(vuz88, vuz89)

The set Q consists of the following terms:

new_sr2(x0, ty_Float)
new_sr0(x0, x1, ty_Int)
new_primPlusNat1(Succ(x0), Succ(x1))
new_primMulNat0(Succ(x0), Zero)
new_primMulNat0(Zero, Zero)
new_sr12(x0, x1)
new_primDivNatS1
new_sr3(x0, app(ty_Ratio, x1))
new_sr3(x0, ty_Float)
new_sr11(Neg(x0), Neg(x1))
new_primPlusNat1(Zero, Zero)
new_sr(x0, x1, ty_Float)
new_sr7(x0)
new_sr0(x0, x1, ty_Integer)
new_sr0(x0, x1, app(ty_Ratio, x2))
new_sr(x0, x1, ty_Int)
new_sr6(x0)
new_sr(x0, x1, ty_Double)
new_sr0(x0, x1, ty_Double)
new_sr9(x0, x1, x2)
new_sr2(x0, ty_Double)
new_sr8(x0)
new_sr(x0, x1, ty_Integer)
new_sr11(Pos(x0), Pos(x1))
new_sr3(x0, ty_Double)
new_primPlusNat1(Succ(x0), Zero)
new_sr3(x0, ty_Int)
new_sr13(Float(x0, x1), Float(x2, x3))
new_sr3(x0, ty_Integer)
new_primDivNatS0(Succ(Succ(x0)))
new_sr11(Pos(x0), Neg(x1))
new_sr11(Neg(x0), Pos(x1))
new_sr2(x0, ty_Integer)
new_primDivNatS0(Zero)
new_primDivNatS0(Succ(Zero))
new_primPlusNat0(Succ(x0), x1)
new_sr2(x0, app(ty_Ratio, x1))
new_sr4(x0, x1)
new_sr5(x0)
new_sr(x0, x1, app(ty_Ratio, x2))
new_primPlusNat1(Zero, Succ(x0))
new_primPlusNat0(Zero, x0)
new_primMulNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Succ(x0))
new_sr10(x0, x1)
new_sr0(x0, x1, ty_Float)
new_sr2(x0, ty_Int)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

new_pr2F0G10(vuz52, vuz53, Succ(Succ(Zero)), bc) → new_pr2F0G11(vuz52, vuz53, Zero, Succ(Zero), bc)
new_pr2F0G1(vuz88, vuz89, vuz90, Succ(Zero), ba) → new_pr2F3(vuz90, vuz88, new_sr(vuz88, vuz89, ba), ba)
new_pr2F0G10(vuz52, vuz53, Succ(Succ(Succ(vuz54000))), bc) → new_pr2F0G11(vuz52, vuz53, new_primDivNatS0(vuz54000), Succ(new_primDivNatS0(vuz54000)), bc)
new_pr2F0G11(vuz64, vuz65, vuz66, Succ(Zero), bd) → new_pr2F3(vuz66, new_sr2(vuz65, bd), vuz64, bd)

The remaining pairs can at least be oriented weakly.

new_pr2F0G1(vuz88, vuz89, vuz90, Succ(Succ(vuz9100)), ba) → new_pr2F0G1(vuz88, vuz89, vuz90, vuz9100, ba)
new_pr2F3(Succ(vuz840), vuz85, vuz86, bb) → new_pr2F0G1(vuz85, vuz86, vuz840, Succ(vuz840), bb)
new_pr2F0G11(vuz64, vuz65, vuz66, Zero, bd) → new_pr2F0G10(vuz64, new_sr3(vuz65, bd), Succ(vuz66), bd)
new_pr2F0G1(vuz88, vuz89, vuz90, Zero, ba) → new_pr2F0G10(new_sr0(vuz88, vuz89, ba), vuz88, Succ(vuz90), ba)
new_pr2F0G11(vuz64, vuz65, vuz66, Succ(Succ(vuz6700)), bd) → new_pr2F0G11(vuz64, vuz65, vuz66, vuz6700, bd)

Used ordering: Polynomial interpretation [25]:

POL(Float(x₁, x₂)) = 1 + x₁ + x₂
POL(Neg(x₁)) = 0
POL(Pos(x₁)) = 0
POL(Succ(x₁)) = 1 + x₁
POL(Zero) = 0
POL([]) = 0
POL(app(x₁, x₂)) = 1 + x₂
POL(error(x₁)) = 0
POL(new_pr2F0G1(x₁, x₂, x₃, x₄, x₅)) = 1 + x₃
POL(new_pr2F0G10(x₁, x₂, x₃, x₄)) = x₃
POL(new_pr2F0G11(x₁, x₂, x₃, x₄, x₅)) = 1 + x₃
POL(new_pr2F3(x₁, x₂, x₃, x₄)) = x₁
POL(new_primDivNatS0(x₁)) = x₁
POL(new_primDivNatS1) = 0
POL(new_primMulNat0(x₁, x₂)) = 0
POL(new_primPlusNat0(x₁, x₂)) = 0
POL(new_primPlusNat1(x₁, x₂)) = 0
POL(new_sr(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(new_sr0(x₁, x₂, x₃)) = x₁ + x₂
POL(new_sr10(x₁, x₂)) = x₁
POL(new_sr11(x₁, x₂)) = 0
POL(new_sr12(x₁, x₂)) = x₂
POL(new_sr13(x₁, x₂)) = x₁ + x₂
POL(new_sr2(x₁, x₂)) = 0
POL(new_sr3(x₁, x₂)) = x₁ + x₂
POL(new_sr4(x₁, x₂)) = 0
POL(new_sr5(x₁)) = 1
POL(new_sr6(x₁)) = 1
POL(new_sr7(x₁)) = 0
POL(new_sr8(x₁)) = 0
POL(new_sr9(x₁, x₂, x₃)) = 0
POL(ty_Double) = 1
POL(ty_Float) = 1
POL(ty_Int) = 1
POL(ty_Integer) = 1
POL(ty_Ratio) = 0

The following usable rules [17] were oriented:

new_primDivNatS1 → Zero
new_primDivNatS0(Succ(Succ(vuz5400000))) → Succ(new_primDivNatS0(vuz5400000))
new_primDivNatS0(Succ(Zero)) → Succ(new_primDivNatS1)
new_primDivNatS0(Zero) → Zero

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ AND

                                ↳ QDP

                                ↳ QDP

                                  ↳ UsableRulesProof

                                    ↳ QDP

                                      ↳ QReductionProof

                                        ↳ QDP

                                          ↳ Rewriting

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ QDPOrderProof

                                                    ↳ QDP

                                                      ↳ DependencyGraphProof

                          ↳ QDP

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_pr2F0G1(vuz88, vuz89, vuz90, Succ(Succ(vuz9100)), ba) → new_pr2F0G1(vuz88, vuz89, vuz90, vuz9100, ba)
new_pr2F3(Succ(vuz840), vuz85, vuz86, bb) → new_pr2F0G1(vuz85, vuz86, vuz840, Succ(vuz840), bb)
new_pr2F0G11(vuz64, vuz65, vuz66, Zero, bd) → new_pr2F0G10(vuz64, new_sr3(vuz65, bd), Succ(vuz66), bd)
new_pr2F0G1(vuz88, vuz89, vuz90, Zero, ba) → new_pr2F0G10(new_sr0(vuz88, vuz89, ba), vuz88, Succ(vuz90), ba)
new_pr2F0G11(vuz64, vuz65, vuz66, Succ(Succ(vuz6700)), bd) → new_pr2F0G11(vuz64, vuz65, vuz66, vuz6700, bd)

The TRS R consists of the following rules:

new_sr0(vuz88, vuz89, ty_Integer) → new_sr12(vuz88, vuz89)
new_sr0(vuz88, vuz89, ty_Double) → new_sr10(vuz88, vuz89)
new_sr0(vuz88, vuz89, app(ty_Ratio, bg)) → new_sr9(vuz88, vuz89, bg)
new_sr0(vuz88, vuz89, ty_Float) → new_sr13(vuz88, vuz89)
new_sr0(vuz88, vuz89, ty_Int) → new_sr11(vuz88, vuz89)
new_sr11(Pos(vuz400), Neg(vuz170)) → Neg(new_primMulNat0(vuz400, vuz170))
new_sr11(Neg(vuz400), Pos(vuz170)) → Neg(new_primMulNat0(vuz400, vuz170))
new_sr11(Neg(vuz400), Neg(vuz170)) → Pos(new_primMulNat0(vuz400, vuz170))
new_sr11(Pos(vuz400), Pos(vuz170)) → Pos(new_primMulNat0(vuz400, vuz170))
new_primMulNat0(Succ(vuz4000), Zero) → Zero
new_primMulNat0(Zero, Succ(vuz1700)) → Zero
new_primMulNat0(Succ(vuz4000), Succ(vuz1700)) → new_primPlusNat0(new_primMulNat0(vuz4000, Succ(vuz1700)), vuz1700)
new_primMulNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(vuz500), vuz1700) → Succ(Succ(new_primPlusNat1(vuz500, vuz1700)))
new_primPlusNat0(Zero, vuz1700) → Succ(vuz1700)
new_primPlusNat1(Succ(vuz5000), Succ(vuz17000)) → Succ(Succ(new_primPlusNat1(vuz5000, vuz17000)))
new_primPlusNat1(Zero, Zero) → Zero
new_primPlusNat1(Zero, Succ(vuz17000)) → Succ(vuz17000)
new_primPlusNat1(Succ(vuz5000), Zero) → Succ(vuz5000)
new_sr13(Float(vuz390, vuz391), Float(vuz170, vuz171)) → Float(new_sr11(vuz390, vuz170), new_sr11(vuz391, vuz171))
new_sr9(vuz13, vuz37, ca) → error([])
new_sr10(vuz41, vuz17) → error([])
new_sr12(vuz38, vuz17) → error([])
new_primDivNatS0(Succ(Succ(vuz5400000))) → Succ(new_primDivNatS0(vuz5400000))
new_primDivNatS0(Succ(Zero)) → Succ(new_primDivNatS1)
new_primDivNatS0(Zero) → Zero
new_primDivNatS1 → Zero
new_sr3(vuz65, ty_Float) → new_sr6(vuz65)
new_sr3(vuz65, ty_Integer) → new_sr5(vuz65)
new_sr3(vuz65, app(ty_Ratio, be)) → new_sr4(vuz65, be)
new_sr3(vuz65, ty_Double) → new_sr8(vuz65)
new_sr3(vuz65, ty_Int) → new_sr7(vuz65)
new_sr7(vuz6) → new_sr11(vuz6, vuz6)
new_sr8(vuz6) → new_sr10(vuz6, vuz6)
new_sr4(vuz6, bf) → new_sr9(vuz6, vuz6, bf)
new_sr5(vuz6) → new_sr12(vuz6, vuz6)
new_sr6(vuz6) → new_sr13(vuz6, vuz6)
new_sr2(vuz65, ty_Integer) → new_sr5(vuz65)
new_sr2(vuz65, ty_Float) → new_sr6(vuz65)
new_sr2(vuz65, ty_Double) → new_sr8(vuz65)
new_sr2(vuz65, ty_Int) → new_sr7(vuz65)
new_sr2(vuz65, app(ty_Ratio, be)) → new_sr4(vuz65, be)
new_sr(vuz88, vuz89, ty_Double) → new_sr10(vuz88, vuz89)
new_sr(vuz88, vuz89, ty_Int) → new_sr11(vuz88, vuz89)
new_sr(vuz88, vuz89, app(ty_Ratio, bg)) → new_sr9(vuz88, vuz89, bg)
new_sr(vuz88, vuz89, ty_Integer) → new_sr12(vuz88, vuz89)
new_sr(vuz88, vuz89, ty_Float) → new_sr13(vuz88, vuz89)

The set Q consists of the following terms:

new_sr2(x0, ty_Float)
new_sr0(x0, x1, ty_Int)
new_primPlusNat1(Succ(x0), Succ(x1))
new_primMulNat0(Succ(x0), Zero)
new_primMulNat0(Zero, Zero)
new_sr12(x0, x1)
new_primDivNatS1
new_sr3(x0, app(ty_Ratio, x1))
new_sr3(x0, ty_Float)
new_sr11(Neg(x0), Neg(x1))
new_primPlusNat1(Zero, Zero)
new_sr(x0, x1, ty_Float)
new_sr7(x0)
new_sr0(x0, x1, ty_Integer)
new_sr0(x0, x1, app(ty_Ratio, x2))
new_sr(x0, x1, ty_Int)
new_sr6(x0)
new_sr(x0, x1, ty_Double)
new_sr0(x0, x1, ty_Double)
new_sr9(x0, x1, x2)
new_sr2(x0, ty_Double)
new_sr8(x0)
new_sr(x0, x1, ty_Integer)
new_sr11(Pos(x0), Pos(x1))
new_sr3(x0, ty_Double)
new_primPlusNat1(Succ(x0), Zero)
new_sr3(x0, ty_Int)
new_sr13(Float(x0, x1), Float(x2, x3))
new_sr3(x0, ty_Integer)
new_primDivNatS0(Succ(Succ(x0)))
new_sr11(Pos(x0), Neg(x1))
new_sr11(Neg(x0), Pos(x1))
new_sr2(x0, ty_Integer)
new_primDivNatS0(Zero)
new_primDivNatS0(Succ(Zero))
new_primPlusNat0(Succ(x0), x1)
new_sr2(x0, app(ty_Ratio, x1))
new_sr4(x0, x1)
new_sr5(x0)
new_sr(x0, x1, app(ty_Ratio, x2))
new_primPlusNat1(Zero, Succ(x0))
new_primPlusNat0(Zero, x0)
new_primMulNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Succ(x0))
new_sr10(x0, x1)
new_sr0(x0, x1, ty_Float)
new_sr2(x0, ty_Int)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 3 less nodes.

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ AND

                                ↳ QDP

                                ↳ QDP

                                  ↳ UsableRulesProof

                                    ↳ QDP

                                      ↳ QReductionProof

                                        ↳ QDP

                                          ↳ Rewriting

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ QDPOrderProof

                                                    ↳ QDP

                                                      ↳ DependencyGraphProof

                                                        ↳ AND

                                                          ↳ QDP

                                                            ↳ UsableRulesProof

                                                          ↳ QDP

                          ↳ QDP

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_pr2F0G11(vuz64, vuz65, vuz66, Succ(Succ(vuz6700)), bd) → new_pr2F0G11(vuz64, vuz65, vuz66, vuz6700, bd)

The TRS R consists of the following rules:

new_sr0(vuz88, vuz89, ty_Integer) → new_sr12(vuz88, vuz89)
new_sr0(vuz88, vuz89, ty_Double) → new_sr10(vuz88, vuz89)
new_sr0(vuz88, vuz89, app(ty_Ratio, bg)) → new_sr9(vuz88, vuz89, bg)
new_sr0(vuz88, vuz89, ty_Float) → new_sr13(vuz88, vuz89)
new_sr0(vuz88, vuz89, ty_Int) → new_sr11(vuz88, vuz89)
new_sr11(Pos(vuz400), Neg(vuz170)) → Neg(new_primMulNat0(vuz400, vuz170))
new_sr11(Neg(vuz400), Pos(vuz170)) → Neg(new_primMulNat0(vuz400, vuz170))
new_sr11(Neg(vuz400), Neg(vuz170)) → Pos(new_primMulNat0(vuz400, vuz170))
new_sr11(Pos(vuz400), Pos(vuz170)) → Pos(new_primMulNat0(vuz400, vuz170))
new_primMulNat0(Succ(vuz4000), Zero) → Zero
new_primMulNat0(Zero, Succ(vuz1700)) → Zero
new_primMulNat0(Succ(vuz4000), Succ(vuz1700)) → new_primPlusNat0(new_primMulNat0(vuz4000, Succ(vuz1700)), vuz1700)
new_primMulNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(vuz500), vuz1700) → Succ(Succ(new_primPlusNat1(vuz500, vuz1700)))
new_primPlusNat0(Zero, vuz1700) → Succ(vuz1700)
new_primPlusNat1(Succ(vuz5000), Succ(vuz17000)) → Succ(Succ(new_primPlusNat1(vuz5000, vuz17000)))
new_primPlusNat1(Zero, Zero) → Zero
new_primPlusNat1(Zero, Succ(vuz17000)) → Succ(vuz17000)
new_primPlusNat1(Succ(vuz5000), Zero) → Succ(vuz5000)
new_sr13(Float(vuz390, vuz391), Float(vuz170, vuz171)) → Float(new_sr11(vuz390, vuz170), new_sr11(vuz391, vuz171))
new_sr9(vuz13, vuz37, ca) → error([])
new_sr10(vuz41, vuz17) → error([])
new_sr12(vuz38, vuz17) → error([])
new_primDivNatS0(Succ(Succ(vuz5400000))) → Succ(new_primDivNatS0(vuz5400000))
new_primDivNatS0(Succ(Zero)) → Succ(new_primDivNatS1)
new_primDivNatS0(Zero) → Zero
new_primDivNatS1 → Zero
new_sr3(vuz65, ty_Float) → new_sr6(vuz65)
new_sr3(vuz65, ty_Integer) → new_sr5(vuz65)
new_sr3(vuz65, app(ty_Ratio, be)) → new_sr4(vuz65, be)
new_sr3(vuz65, ty_Double) → new_sr8(vuz65)
new_sr3(vuz65, ty_Int) → new_sr7(vuz65)
new_sr7(vuz6) → new_sr11(vuz6, vuz6)
new_sr8(vuz6) → new_sr10(vuz6, vuz6)
new_sr4(vuz6, bf) → new_sr9(vuz6, vuz6, bf)
new_sr5(vuz6) → new_sr12(vuz6, vuz6)
new_sr6(vuz6) → new_sr13(vuz6, vuz6)
new_sr2(vuz65, ty_Integer) → new_sr5(vuz65)
new_sr2(vuz65, ty_Float) → new_sr6(vuz65)
new_sr2(vuz65, ty_Double) → new_sr8(vuz65)
new_sr2(vuz65, ty_Int) → new_sr7(vuz65)
new_sr2(vuz65, app(ty_Ratio, be)) → new_sr4(vuz65, be)
new_sr(vuz88, vuz89, ty_Double) → new_sr10(vuz88, vuz89)
new_sr(vuz88, vuz89, ty_Int) → new_sr11(vuz88, vuz89)
new_sr(vuz88, vuz89, app(ty_Ratio, bg)) → new_sr9(vuz88, vuz89, bg)
new_sr(vuz88, vuz89, ty_Integer) → new_sr12(vuz88, vuz89)
new_sr(vuz88, vuz89, ty_Float) → new_sr13(vuz88, vuz89)

The set Q consists of the following terms:

new_sr2(x0, ty_Float)
new_sr0(x0, x1, ty_Int)
new_primPlusNat1(Succ(x0), Succ(x1))
new_primMulNat0(Succ(x0), Zero)
new_primMulNat0(Zero, Zero)
new_sr12(x0, x1)
new_primDivNatS1
new_sr3(x0, app(ty_Ratio, x1))
new_sr3(x0, ty_Float)
new_sr11(Neg(x0), Neg(x1))
new_primPlusNat1(Zero, Zero)
new_sr(x0, x1, ty_Float)
new_sr7(x0)
new_sr0(x0, x1, ty_Integer)
new_sr0(x0, x1, app(ty_Ratio, x2))
new_sr(x0, x1, ty_Int)
new_sr6(x0)
new_sr(x0, x1, ty_Double)
new_sr0(x0, x1, ty_Double)
new_sr9(x0, x1, x2)
new_sr2(x0, ty_Double)
new_sr8(x0)
new_sr(x0, x1, ty_Integer)
new_sr11(Pos(x0), Pos(x1))
new_sr3(x0, ty_Double)
new_primPlusNat1(Succ(x0), Zero)
new_sr3(x0, ty_Int)
new_sr13(Float(x0, x1), Float(x2, x3))
new_sr3(x0, ty_Integer)
new_primDivNatS0(Succ(Succ(x0)))
new_sr11(Pos(x0), Neg(x1))
new_sr11(Neg(x0), Pos(x1))
new_sr2(x0, ty_Integer)
new_primDivNatS0(Zero)
new_primDivNatS0(Succ(Zero))
new_primPlusNat0(Succ(x0), x1)
new_sr2(x0, app(ty_Ratio, x1))
new_sr4(x0, x1)
new_sr5(x0)
new_sr(x0, x1, app(ty_Ratio, x2))
new_primPlusNat1(Zero, Succ(x0))
new_primPlusNat0(Zero, x0)
new_primMulNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Succ(x0))
new_sr10(x0, x1)
new_sr0(x0, x1, ty_Float)
new_sr2(x0, ty_Int)

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ AND

                                ↳ QDP

                                ↳ QDP

                                  ↳ UsableRulesProof

                                    ↳ QDP

                                      ↳ QReductionProof

                                        ↳ QDP

                                          ↳ Rewriting

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ QDPOrderProof

                                                    ↳ QDP

                                                      ↳ DependencyGraphProof

                                                        ↳ AND

                                                          ↳ QDP

                                                            ↳ UsableRulesProof

                                                              ↳ QDP

                                                                ↳ QReductionProof

                                                          ↳ QDP

                          ↳ QDP

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_pr2F0G11(vuz64, vuz65, vuz66, Succ(Succ(vuz6700)), bd) → new_pr2F0G11(vuz64, vuz65, vuz66, vuz6700, bd)

R is empty.
The set Q consists of the following terms:

new_sr2(x0, ty_Float)
new_sr0(x0, x1, ty_Int)
new_primPlusNat1(Succ(x0), Succ(x1))
new_primMulNat0(Succ(x0), Zero)
new_primMulNat0(Zero, Zero)
new_sr12(x0, x1)
new_primDivNatS1
new_sr3(x0, app(ty_Ratio, x1))
new_sr3(x0, ty_Float)
new_sr11(Neg(x0), Neg(x1))
new_primPlusNat1(Zero, Zero)
new_sr(x0, x1, ty_Float)
new_sr7(x0)
new_sr0(x0, x1, ty_Integer)
new_sr0(x0, x1, app(ty_Ratio, x2))
new_sr(x0, x1, ty_Int)
new_sr6(x0)
new_sr(x0, x1, ty_Double)
new_sr0(x0, x1, ty_Double)
new_sr9(x0, x1, x2)
new_sr2(x0, ty_Double)
new_sr8(x0)
new_sr(x0, x1, ty_Integer)
new_sr11(Pos(x0), Pos(x1))
new_sr3(x0, ty_Double)
new_primPlusNat1(Succ(x0), Zero)
new_sr3(x0, ty_Int)
new_sr13(Float(x0, x1), Float(x2, x3))
new_sr3(x0, ty_Integer)
new_primDivNatS0(Succ(Succ(x0)))
new_sr11(Pos(x0), Neg(x1))
new_sr11(Neg(x0), Pos(x1))
new_sr2(x0, ty_Integer)
new_primDivNatS0(Zero)
new_primDivNatS0(Succ(Zero))
new_primPlusNat0(Succ(x0), x1)
new_sr2(x0, app(ty_Ratio, x1))
new_sr4(x0, x1)
new_sr5(x0)
new_sr(x0, x1, app(ty_Ratio, x2))
new_primPlusNat1(Zero, Succ(x0))
new_primPlusNat0(Zero, x0)
new_primMulNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Succ(x0))
new_sr10(x0, x1)
new_sr0(x0, x1, ty_Float)
new_sr2(x0, ty_Int)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_sr2(x0, ty_Float)
new_sr0(x0, x1, ty_Int)
new_primPlusNat1(Succ(x0), Succ(x1))
new_primMulNat0(Succ(x0), Zero)
new_primMulNat0(Zero, Zero)
new_sr12(x0, x1)
new_primDivNatS1
new_sr3(x0, app(ty_Ratio, x1))
new_sr3(x0, ty_Float)
new_sr11(Neg(x0), Neg(x1))
new_primPlusNat1(Zero, Zero)
new_sr(x0, x1, ty_Float)
new_sr7(x0)
new_sr0(x0, x1, ty_Integer)
new_sr0(x0, x1, app(ty_Ratio, x2))
new_sr(x0, x1, ty_Int)
new_sr6(x0)
new_sr(x0, x1, ty_Double)
new_sr0(x0, x1, ty_Double)
new_sr9(x0, x1, x2)
new_sr2(x0, ty_Double)
new_sr8(x0)
new_sr(x0, x1, ty_Integer)
new_sr11(Pos(x0), Pos(x1))
new_sr3(x0, ty_Double)
new_primPlusNat1(Succ(x0), Zero)
new_sr3(x0, ty_Int)
new_sr13(Float(x0, x1), Float(x2, x3))
new_sr3(x0, ty_Integer)
new_primDivNatS0(Succ(Succ(x0)))
new_sr11(Pos(x0), Neg(x1))
new_sr11(Neg(x0), Pos(x1))
new_sr2(x0, ty_Integer)
new_primDivNatS0(Zero)
new_primDivNatS0(Succ(Zero))
new_primPlusNat0(Succ(x0), x1)
new_sr2(x0, app(ty_Ratio, x1))
new_sr4(x0, x1)
new_sr5(x0)
new_sr(x0, x1, app(ty_Ratio, x2))
new_primPlusNat1(Zero, Succ(x0))
new_primPlusNat0(Zero, x0)
new_primMulNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Succ(x0))
new_sr10(x0, x1)
new_sr0(x0, x1, ty_Float)
new_sr2(x0, ty_Int)

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ AND

                                ↳ QDP

                                ↳ QDP

                                  ↳ UsableRulesProof

                                    ↳ QDP

                                      ↳ QReductionProof

                                        ↳ QDP

                                          ↳ Rewriting

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ QDPOrderProof

                                                    ↳ QDP

                                                      ↳ DependencyGraphProof

                                                        ↳ AND

                                                          ↳ QDP

                                                            ↳ UsableRulesProof

                                                              ↳ QDP

                                                                ↳ QReductionProof

                                                                  ↳ QDP

                                                                    ↳ QDPSizeChangeProof

                                                          ↳ QDP

                          ↳ QDP

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_pr2F0G11(vuz64, vuz65, vuz66, Succ(Succ(vuz6700)), bd) → new_pr2F0G11(vuz64, vuz65, vuz66, vuz6700, bd)

From the DPs we obtained the following set of size-change graphs:

new_pr2F0G11(vuz64, vuz65, vuz66, Succ(Succ(vuz6700)), bd) → new_pr2F0G11(vuz64, vuz65, vuz66, vuz6700, bd)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 > 4, 5 >= 5

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ AND

                                ↳ QDP

                                ↳ QDP

                                  ↳ UsableRulesProof

                                    ↳ QDP

                                      ↳ QReductionProof

                                        ↳ QDP

                                          ↳ Rewriting

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ QDPOrderProof

                                                    ↳ QDP

                                                      ↳ DependencyGraphProof

                                                        ↳ AND

                                                          ↳ QDP

                                                          ↳ QDP

                                                            ↳ UsableRulesProof

                          ↳ QDP

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_pr2F0G1(vuz88, vuz89, vuz90, Succ(Succ(vuz9100)), ba) → new_pr2F0G1(vuz88, vuz89, vuz90, vuz9100, ba)

The TRS R consists of the following rules:

new_sr0(vuz88, vuz89, ty_Integer) → new_sr12(vuz88, vuz89)
new_sr0(vuz88, vuz89, ty_Double) → new_sr10(vuz88, vuz89)
new_sr0(vuz88, vuz89, app(ty_Ratio, bg)) → new_sr9(vuz88, vuz89, bg)
new_sr0(vuz88, vuz89, ty_Float) → new_sr13(vuz88, vuz89)
new_sr0(vuz88, vuz89, ty_Int) → new_sr11(vuz88, vuz89)
new_sr11(Pos(vuz400), Neg(vuz170)) → Neg(new_primMulNat0(vuz400, vuz170))
new_sr11(Neg(vuz400), Pos(vuz170)) → Neg(new_primMulNat0(vuz400, vuz170))
new_sr11(Neg(vuz400), Neg(vuz170)) → Pos(new_primMulNat0(vuz400, vuz170))
new_sr11(Pos(vuz400), Pos(vuz170)) → Pos(new_primMulNat0(vuz400, vuz170))
new_primMulNat0(Succ(vuz4000), Zero) → Zero
new_primMulNat0(Zero, Succ(vuz1700)) → Zero
new_primMulNat0(Succ(vuz4000), Succ(vuz1700)) → new_primPlusNat0(new_primMulNat0(vuz4000, Succ(vuz1700)), vuz1700)
new_primMulNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(vuz500), vuz1700) → Succ(Succ(new_primPlusNat1(vuz500, vuz1700)))
new_primPlusNat0(Zero, vuz1700) → Succ(vuz1700)
new_primPlusNat1(Succ(vuz5000), Succ(vuz17000)) → Succ(Succ(new_primPlusNat1(vuz5000, vuz17000)))
new_primPlusNat1(Zero, Zero) → Zero
new_primPlusNat1(Zero, Succ(vuz17000)) → Succ(vuz17000)
new_primPlusNat1(Succ(vuz5000), Zero) → Succ(vuz5000)
new_sr13(Float(vuz390, vuz391), Float(vuz170, vuz171)) → Float(new_sr11(vuz390, vuz170), new_sr11(vuz391, vuz171))
new_sr9(vuz13, vuz37, ca) → error([])
new_sr10(vuz41, vuz17) → error([])
new_sr12(vuz38, vuz17) → error([])
new_primDivNatS0(Succ(Succ(vuz5400000))) → Succ(new_primDivNatS0(vuz5400000))
new_primDivNatS0(Succ(Zero)) → Succ(new_primDivNatS1)
new_primDivNatS0(Zero) → Zero
new_primDivNatS1 → Zero
new_sr3(vuz65, ty_Float) → new_sr6(vuz65)
new_sr3(vuz65, ty_Integer) → new_sr5(vuz65)
new_sr3(vuz65, app(ty_Ratio, be)) → new_sr4(vuz65, be)
new_sr3(vuz65, ty_Double) → new_sr8(vuz65)
new_sr3(vuz65, ty_Int) → new_sr7(vuz65)
new_sr7(vuz6) → new_sr11(vuz6, vuz6)
new_sr8(vuz6) → new_sr10(vuz6, vuz6)
new_sr4(vuz6, bf) → new_sr9(vuz6, vuz6, bf)
new_sr5(vuz6) → new_sr12(vuz6, vuz6)
new_sr6(vuz6) → new_sr13(vuz6, vuz6)
new_sr2(vuz65, ty_Integer) → new_sr5(vuz65)
new_sr2(vuz65, ty_Float) → new_sr6(vuz65)
new_sr2(vuz65, ty_Double) → new_sr8(vuz65)
new_sr2(vuz65, ty_Int) → new_sr7(vuz65)
new_sr2(vuz65, app(ty_Ratio, be)) → new_sr4(vuz65, be)
new_sr(vuz88, vuz89, ty_Double) → new_sr10(vuz88, vuz89)
new_sr(vuz88, vuz89, ty_Int) → new_sr11(vuz88, vuz89)
new_sr(vuz88, vuz89, app(ty_Ratio, bg)) → new_sr9(vuz88, vuz89, bg)
new_sr(vuz88, vuz89, ty_Integer) → new_sr12(vuz88, vuz89)
new_sr(vuz88, vuz89, ty_Float) → new_sr13(vuz88, vuz89)

The set Q consists of the following terms:

new_sr2(x0, ty_Float)
new_sr0(x0, x1, ty_Int)
new_primPlusNat1(Succ(x0), Succ(x1))
new_primMulNat0(Succ(x0), Zero)
new_primMulNat0(Zero, Zero)
new_sr12(x0, x1)
new_primDivNatS1
new_sr3(x0, app(ty_Ratio, x1))
new_sr3(x0, ty_Float)
new_sr11(Neg(x0), Neg(x1))
new_primPlusNat1(Zero, Zero)
new_sr(x0, x1, ty_Float)
new_sr7(x0)
new_sr0(x0, x1, ty_Integer)
new_sr0(x0, x1, app(ty_Ratio, x2))
new_sr(x0, x1, ty_Int)
new_sr6(x0)
new_sr(x0, x1, ty_Double)
new_sr0(x0, x1, ty_Double)
new_sr9(x0, x1, x2)
new_sr2(x0, ty_Double)
new_sr8(x0)
new_sr(x0, x1, ty_Integer)
new_sr11(Pos(x0), Pos(x1))
new_sr3(x0, ty_Double)
new_primPlusNat1(Succ(x0), Zero)
new_sr3(x0, ty_Int)
new_sr13(Float(x0, x1), Float(x2, x3))
new_sr3(x0, ty_Integer)
new_primDivNatS0(Succ(Succ(x0)))
new_sr11(Pos(x0), Neg(x1))
new_sr11(Neg(x0), Pos(x1))
new_sr2(x0, ty_Integer)
new_primDivNatS0(Zero)
new_primDivNatS0(Succ(Zero))
new_primPlusNat0(Succ(x0), x1)
new_sr2(x0, app(ty_Ratio, x1))
new_sr4(x0, x1)
new_sr5(x0)
new_sr(x0, x1, app(ty_Ratio, x2))
new_primPlusNat1(Zero, Succ(x0))
new_primPlusNat0(Zero, x0)
new_primMulNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Succ(x0))
new_sr10(x0, x1)
new_sr0(x0, x1, ty_Float)
new_sr2(x0, ty_Int)

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ AND

                                ↳ QDP

                                ↳ QDP

                                  ↳ UsableRulesProof

                                    ↳ QDP

                                      ↳ QReductionProof

                                        ↳ QDP

                                          ↳ Rewriting

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ QDPOrderProof

                                                    ↳ QDP

                                                      ↳ DependencyGraphProof

                                                        ↳ AND

                                                          ↳ QDP

                                                          ↳ QDP

                                                            ↳ UsableRulesProof

                                                              ↳ QDP

                                                                ↳ QReductionProof

                          ↳ QDP

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_pr2F0G1(vuz88, vuz89, vuz90, Succ(Succ(vuz9100)), ba) → new_pr2F0G1(vuz88, vuz89, vuz90, vuz9100, ba)

R is empty.
The set Q consists of the following terms:

new_sr2(x0, ty_Float)
new_sr0(x0, x1, ty_Int)
new_primPlusNat1(Succ(x0), Succ(x1))
new_primMulNat0(Succ(x0), Zero)
new_primMulNat0(Zero, Zero)
new_sr12(x0, x1)
new_primDivNatS1
new_sr3(x0, app(ty_Ratio, x1))
new_sr3(x0, ty_Float)
new_sr11(Neg(x0), Neg(x1))
new_primPlusNat1(Zero, Zero)
new_sr(x0, x1, ty_Float)
new_sr7(x0)
new_sr0(x0, x1, ty_Integer)
new_sr0(x0, x1, app(ty_Ratio, x2))
new_sr(x0, x1, ty_Int)
new_sr6(x0)
new_sr(x0, x1, ty_Double)
new_sr0(x0, x1, ty_Double)
new_sr9(x0, x1, x2)
new_sr2(x0, ty_Double)
new_sr8(x0)
new_sr(x0, x1, ty_Integer)
new_sr11(Pos(x0), Pos(x1))
new_sr3(x0, ty_Double)
new_primPlusNat1(Succ(x0), Zero)
new_sr3(x0, ty_Int)
new_sr13(Float(x0, x1), Float(x2, x3))
new_sr3(x0, ty_Integer)
new_primDivNatS0(Succ(Succ(x0)))
new_sr11(Pos(x0), Neg(x1))
new_sr11(Neg(x0), Pos(x1))
new_sr2(x0, ty_Integer)
new_primDivNatS0(Zero)
new_primDivNatS0(Succ(Zero))
new_primPlusNat0(Succ(x0), x1)
new_sr2(x0, app(ty_Ratio, x1))
new_sr4(x0, x1)
new_sr5(x0)
new_sr(x0, x1, app(ty_Ratio, x2))
new_primPlusNat1(Zero, Succ(x0))
new_primPlusNat0(Zero, x0)
new_primMulNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Succ(x0))
new_sr10(x0, x1)
new_sr0(x0, x1, ty_Float)
new_sr2(x0, ty_Int)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_sr2(x0, ty_Float)
new_sr0(x0, x1, ty_Int)
new_primPlusNat1(Succ(x0), Succ(x1))
new_primMulNat0(Succ(x0), Zero)
new_primMulNat0(Zero, Zero)
new_sr12(x0, x1)
new_primDivNatS1
new_sr3(x0, app(ty_Ratio, x1))
new_sr3(x0, ty_Float)
new_sr11(Neg(x0), Neg(x1))
new_primPlusNat1(Zero, Zero)
new_sr(x0, x1, ty_Float)
new_sr7(x0)
new_sr0(x0, x1, ty_Integer)
new_sr0(x0, x1, app(ty_Ratio, x2))
new_sr(x0, x1, ty_Int)
new_sr6(x0)
new_sr(x0, x1, ty_Double)
new_sr0(x0, x1, ty_Double)
new_sr9(x0, x1, x2)
new_sr2(x0, ty_Double)
new_sr8(x0)
new_sr(x0, x1, ty_Integer)
new_sr11(Pos(x0), Pos(x1))
new_sr3(x0, ty_Double)
new_primPlusNat1(Succ(x0), Zero)
new_sr3(x0, ty_Int)
new_sr13(Float(x0, x1), Float(x2, x3))
new_sr3(x0, ty_Integer)
new_primDivNatS0(Succ(Succ(x0)))
new_sr11(Pos(x0), Neg(x1))
new_sr11(Neg(x0), Pos(x1))
new_sr2(x0, ty_Integer)
new_primDivNatS0(Zero)
new_primDivNatS0(Succ(Zero))
new_primPlusNat0(Succ(x0), x1)
new_sr2(x0, app(ty_Ratio, x1))
new_sr4(x0, x1)
new_sr5(x0)
new_sr(x0, x1, app(ty_Ratio, x2))
new_primPlusNat1(Zero, Succ(x0))
new_primPlusNat0(Zero, x0)
new_primMulNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Succ(x0))
new_sr10(x0, x1)
new_sr0(x0, x1, ty_Float)
new_sr2(x0, ty_Int)

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ AND

                                ↳ QDP

                                ↳ QDP

                                  ↳ UsableRulesProof

                                    ↳ QDP

                                      ↳ QReductionProof

                                        ↳ QDP

                                          ↳ Rewriting

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ QDPOrderProof

                                                    ↳ QDP

                                                      ↳ DependencyGraphProof

                                                        ↳ AND

                                                          ↳ QDP

                                                          ↳ QDP

                                                            ↳ UsableRulesProof

                                                              ↳ QDP

                                                                ↳ QReductionProof

                                                                  ↳ QDP

                                                                    ↳ QDPSizeChangeProof

                          ↳ QDP

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_pr2F0G1(vuz88, vuz89, vuz90, Succ(Succ(vuz9100)), ba) → new_pr2F0G1(vuz88, vuz89, vuz90, vuz9100, ba)

From the DPs we obtained the following set of size-change graphs:

new_pr2F0G1(vuz88, vuz89, vuz90, Succ(Succ(vuz9100)), ba) → new_pr2F0G1(vuz88, vuz89, vuz90, vuz9100, ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 > 4, 5 >= 5

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ QDPSizeChangeProof

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_pr2F0G13(vuz6, vuz7, Succ(Succ(vuz800)), ba) → new_pr2F0G13(vuz6, vuz7, vuz800, ba)

From the DPs we obtained the following set of size-change graphs:

new_pr2F0G13(vuz6, vuz7, Succ(Succ(vuz800)), ba) → new_pr2F0G13(vuz6, vuz7, vuz800, ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 >= 4

Haskell To QDPs

primDivNatS0	x y True	= Succ (primDivNatS (primMinusNatS x y) (Succ y))
primDivNatS0	x y False	= Zero

g1	x n True	= g (x * x) (n `quot` 2)
g1	x n False	= g0 x n otherwise

pr2F4	vv yu y	= pr2F3 (yu == 0) vv yu y
pr2F4	yz zu zv	= pr2F0 yz zu zv

pr2F0G1	vuy x n True	= pr2F0G vuy (x * x) (n `quot` 2)
pr2F0G1	vuy x n False	= pr2F0G0 vuy x n otherwise